Encoding Peano arithmetic in a minimal fragment of separation logic
From MaRDI portal
Cites work
- A decidable fragment in separation logic with inductive predicates and arithmetic
- A decision procedure for satisfiability in separation logic with inductive predicates
- An undecidability result for separation logic with theory reasoning
- Beyond symbolic heaps: deciding separation logic with inductive definitions
- Completeness of cyclic proofs for symbolic heaps with inductive definitions
- Compositional shape analysis by means of bi-abduction
- Decidability for entailments of symbolic heaps with arrays
- Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
- Foundations for decision problems in separation logic with general inductive predicates
- Foundations of Software Science and Computational Structures
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- scientific article; zbMATH DE number 2081098 (Why is no real title available?)
- scientific article; zbMATH DE number 803291 (Why is no real title available?)
- scientific article; zbMATH DE number 3248792 (Why is no real title available?)
- On the almighty wand
- Programming Languages and Systems
- Representation of Peano arithmetic in separation logic
- Separation logic with monadic inductive definitions and implicit existentials
- The tree width of separation logic with recursive definitions
- Tractable Reasoning in a Fragment of Separation Logic
- Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt.
This page was built for publication: Encoding Peano arithmetic in a minimal fragment of separation logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7255002)
