Verifiable and Executable Logic Specifications of Concurrent Objects in Lpi
No abstract available.
Related papers
- Verifying Executable Object-Oriented Specifications with Separation Logic ECOOP 2010
- A Proof Recipe for Linearizability in Relaxed Memory Separation Logic PLDI 2024
- LPI: Software Verification with Local Policy Iteration - (Competition Contribution) TACAS 2016
- Progress of concurrent objects with partial methods POPL 2018
- Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking VMCAI 2004
- A program logic for concurrent objects under fair scheduling POPL 2016
- Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity ESOP 2015
- Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning ECOOP 2024