Automated Cyclic Entailment Proofs in Separation Logic
From MaRDI portal
Publication:5200020
DOI10.1007/978-3-642-22438-6_12zbMath1341.68184OpenAlexW32928793MaRDI QIDQ5200020
Dino Distefano, James Brotherston, Rasmus L. Petersen
Publication date: 29 July 2011
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-22438-6_12
Related Items
Program Verification with Separation Logic, Soundness and completeness proofs by coinductive methods, A First-Order Logic with Frames, Automated Theorem Proving for Assertions in Separation Logic with All Connectives, Completeness for a First-Order Abstract Separation Logic, Unnamed Item, Unnamed Item, Automated mutual induction proof in separation logic, Completeness and expressiveness of pointer program verification by separation logic, Cyclic hypersequent system for transitive closure logic, An efficient cyclic entailment procedure in a fragment of separation logic, Abstract cyclic proofs, Cyclic Arithmetic Is Equivalent to Peano Arithmetic, Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System, Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic, Contributed papers. Restriction on cut in cyclic proof system for symbolic heaps, Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs, Unnamed Item, A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints, Non-well-founded deduction for induction and coinduction, Cyclic proofs, hypersequents, and transitive closure logic, A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
Uses Software
Cites Work
- Unnamed Item
- Sequent calculi for induction and infinite descent
- HOL Light: An Overview
- A Formalisation of Smallfoot in HOL
- Undecidability of Propositional Separation Logic and Its Neighbours
- Cyclic proofs of program termination in separation logic
- Relational inductive shape analysis
- Enhancing Program Verification with Lemmas
- Scalable Shape Analysis for Systems Code
- Formalised Inductive Reasoning in the Logic of Bunched Implications
- Descente Infinie + Deduction
- Compositional shape analysis by means of bi-abduction
- Automated Verification of Shape and Size Properties Via Separation Logic
- Theorem Proving in Higher Order Logics
- Tools and Algorithms for the Construction and Analysis of Systems
