Automatically verifying temporal properties of pointer programs with cyclic proof
From MaRDI portal
Publication:5919481
DOI10.1007/s10817-019-09532-0zbMath1468.68137OpenAlexW2967943502WikidataQ127392044 ScholiaQ127392044MaRDI QIDQ5919481
James Brotherston, Gadi Tellez
Publication date: 3 March 2020
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-019-09532-0
Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
Uniform interpolation from cyclic proofs: the case of modal mu-calculus, Cyclic hypersequent system for transitive closure logic, Cyclic proofs, hypersequents, and transitive closure logic, Loop-check specification for a sequent calculus of temporal logic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Completing the temporal picture
- On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems
- Practical CTL* model checking: Should SPIN be extended?
- Verification of concurrent programs: The automata-theoretic framework
- Proving that programs eventually do something good
- Cyclic proofs of program termination in separation logic
- A Marriage of Rely/Guarantee and Separation Logic
- Formalised Inductive Reasoning in the Logic of Bunched Implications
- “Sometimes” and “not never” revisited
- Proving the Correctness of Multiprocess Programs
- Verification of temporal properties
- Automatic numeric abstractions for heap-manipulating programs
- Tools and Algorithms for the Construction and Analysis of Systems
- Making prophecies with decision predicates
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Automatically verifying temporal properties of pointer programs with cyclic proof
