Using a Theorem Prover for Reasoning about Concurrent Algorithms
No abstract available.
Related papers
- HOLCF=HOL+LCF JFP 1999
- Reasoning About Programs POPL 1973
- Mechanically verified proof obligations for linearizability TOPLAS 2011
- Separation logic + superposition calculus = heap theorem prover PLDI 2011
- Owicki-Gries Reasoning for C11 RAR ECOOP 2020
- Reasoning about Java Classes (Preliminary Report) OOPSLA 1998
- Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation POPL 2026
- Liquid Amortization: Proving Amortized Complexity with LiquidHaskell (Functional Pearl) Haskell 2024