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

cyclic proofHoare logicinductive definitionsprogram verificationseparation logictermination

Mathematics Subject Classification ID

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

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

(27)

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

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)