Cyclic proofs of program termination in separation logic

DOI10.1145/1328438.1328453MaRDI QIDQ3189830zbMATH OpenOpenAlexWikidataFDO

Authors James Brotherston, Richard Bornat, Cristiano Calcagno

Publication date 12 September 2014

Published in Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1328438.1328453

zbMATH Keywords

Hoare logicprogram verificationseparation logicterminationinductive definitionscyclic proof

Mathematics Subject Classification ID

Graph theory (including graph drawing) in computer science (68R10) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Recommendations

• Automatic Termination Proofs for Programs with Shape-Shifting Heaps
• Automated cyclic entailment proofs in separation logic
• Propositional reasoning about safety and termination of heap-manipulating programs
• Separation logic adapted for proofs by rewriting
• scientific article; zbMATH DE number 1903370

Cited in

(25)

• Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
• Inference of field-sensitive reachability and cyclicity
• Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent
• Propositional reasoning about safety and termination of heap-manipulating programs
• scientific article; zbMATH DE number 7155168 (Why is no real title available?)
• Completeness and expressiveness of pointer program verification by separation logic
• Automatic Termination Proofs for Programs with Shape-Shifting Heaps
• Procedural representation of CIC proof terms
• scientific article; zbMATH DE number 7089071 (Why is no real title available?)
• Soundness and completeness proofs by coinductive methods
• scientific article; zbMATH DE number 7453196 (Why is no real title available?)
• scientific article; zbMATH DE number 7439738 (Why is no real title available?)
• Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
• Non-well-founded deduction for induction and coinduction
• Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs
• Integrating induction and coinduction via closure operators and proof cycles
• Fragments of arithmetic and cyclic proofs
• Automated cyclic entailment proofs in separation logic
• From shape analysis to termination analysis in linear time
• Cyclic arithmetic is equivalent to Peano arithmetic
• The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
• Heap Assumptions on Demand
• Automatically verifying temporal properties of pointer programs with cyclic proof
• Realizability in cyclic proof: extracting ordering information for infinite descent
• Completeness of cyclic proofs for symbolic heaps with inductive definitions

This page was built for publication: Cyclic proofs of program termination in separation logic

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