Automatically verifying temporal properties of pointer programs with cyclic proof
From MaRDI portal
Publication:5920091
DOI10.1007/978-3-319-63046-5_30zbMath1468.68136OpenAlexW2735988056MaRDI QIDQ5920091
James Brotherston, Gadi Tellez
Publication date: 22 September 2017
Published in: Automated Deduction – CADE 26 (Search for Journal in Brave)
Full work available at URL: https://discovery.ucl.ac.uk/id/eprint/10087494/
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
Cyclic hypersequent system for transitive closure logic ⋮ Abstract cyclic proofs ⋮ Automatically verifying temporal properties of pointer programs with cyclic proof ⋮ Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent ⋮ Non-well-founded deduction for induction and coinduction ⋮ Integrating induction and coinduction via closure operators and proof cycles ⋮ Cyclic proofs, hypersequents, and transitive closure logic
Uses Software
