Verifying Executable Object-Oriented Specifications with Separation Logic
No abstract available.
Related papers
- A Proof Recipe for Linearizability in Relaxed Memory Separation Logic PLDI 2024
- jStar: towards practical verification for java OOPSLA 2008
- Verifiable and Executable Logic Specifications of Concurrent Objects in Lpi ESOP 1998
- Reasoning about multiple related abstractions with MultiStar OOPSLA 2010
- A logic for information flow in object-oriented programs POPL 2006
- JaVerT: JavaScript verification toolchain POPL 2018
- Enhancing modular OO verification with separation logic POPL 2008
- Verified symbolic execution with Kripke specification monads (and no meta-programming) ICFP 2022