Automatically verifying temporal properties of pointer programs with cyclic proof

DOI10.1007/978-3-319-63046-5_30MaRDI QIDQ5920091zbMATH OpenOpenAlexFDO

Authors G. Téllez, James Brotherston

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/

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Automatically verifying temporal properties of pointer programs with cyclic proof
• Automated verification of recursive programs with pointers
• scientific article; zbMATH DE number 1956491
• Reasoning About Sequences of Memory States
• Automated cyclic entailment proofs in separation logic

Cited in

(12)

• 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
• Automated verification of recursive programs with pointers
• scientific article; zbMATH DE number 1956491 (Why is no real title available?)
• Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent
• Automatically verifying temporal properties of pointer programs with cyclic proof
• Cyclic hypersequent system for transitive closure logic
• Abstract cyclic proofs
• Per-dereference verification of temporal heap safety via adaptive context-sensitive analysis
• Temporal verification of programs via first-order fixpoint logic
• Abstract cyclic proofs

Describes a project that uses

Uses Software

• BLAST

This page was built for publication: Automatically verifying temporal properties of pointer programs with cyclic proof

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5920091)