Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library
Abstract elided by the publisher.
Related papers
- Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness OOPSLA 2025
- Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency ICFP 2013
- Lawyer: Modular Obligations-Based Liveness Reasoning in Higher-Order Impredicative Concurrent Separation Logic OOPSLA 2026
- Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs ICFP 2025
- A Separation Logic for Parallel Time Complexity with Work and Span Credits ICFP 2026
- Verifying a hash table and its iterators in higher-order separation logic CPP 2017
- Generic Refinement Types POPL 2025
- Raven: An SMT-Based Concurrency Verifier CAV 2025