Automated and Modular Refinement Reasoning for Concurrent Programs
Abstract elided by the publisher.
Related papers
- Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency ICFP 2013
- RefinedC: automating the foundational verification of C code with refined ownership types PLDI 2021
- Caper - Automatic Verification for Fine-Grained Concurrency ESOP 2017
- Raven: An SMT-Based Concurrency Verifier CAV 2025
- Lawyer: Modular Obligations-Based Liveness Reasoning in Higher-Order Impredicative Concurrent Separation Logic OOPSLA 2026
- Automated Assume-Guarantee Reasoning by Abstraction Refinement CAV 2008
- Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement POPL 2024
- Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness OOPSLA 2025