The Teaching Tool CalcCheck A Proof-Checker for Gries and Schneider's "Logical Approach to Discrete Math"
No abstract available.
DOI 10.1007/978-3-642-25379-9_17
Related papers
- Owicki-Gries Reasoning for C11 RAR ECOOP 2020
- View-Based Owicki-Gries Reasoning for Persistent x86-TSO ESOP 2022
- nekton: A Linearizability Proof Checker CAV 2023
- Lean-Auto: An Interface Between Lean 4 and Automated Theorem Provers CAV 2025
- Subjective auxiliary state for coarse-grained concurrency POPL 2013
- Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86 OOPSLA 2020
- Synthesis of Resource Invariants for Concurrent Programs TOPLAS 1980
- Synthesis of Resource Invariants for Concurrent Programs POPL 1979