Cyclic proofs of program termination in separation logic

DOI10.1145/1328438.1328453zbMath1295.68156MaRDI QIDQ3189830

Cristiano Calcagno, James Brotherston, Richard Bornat

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

termination; Hoare logic; separation logic; program verification; inductive definitions; cyclic proof

Mathematics Subject Classification ID

68R10: Graph theory (including graph drawing) in computer science

03B70: Logic in computer science

68Q55: Semantics in the theory of computing

68Q60: Specification and verification (program logics, model checking, etc.)

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Automated Cyclic Entailment Proofs in Separation Logic, Automatically verifying temporal properties of pointer programs with cyclic proof, Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper), Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs, Non-well-founded deduction for induction and coinduction, Soundness and completeness proofs by coinductive methods, Completeness and expressiveness of pointer program verification by separation logic, 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