CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs
No abstract available.
Related papers
- CSim2: Compositional Top-down Verification of Concurrent Systems using Rely-Guarantee TOPLAS 2021
- A rely-guarantee-based simulation for verifying concurrent program transformations POPL 2012
- Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations TOPLAS 2014
- A program logic for concurrent objects under fair scheduling POPL 2016
- Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement Types TOPLAS 2017
- DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs POPL 2026
- Modular verification of concurrent assembly code with dynamic thread creation and termination ICFP 2005
- Local rely-guarantee reasoning POPL 2009