A decidable fragment of separation logic
From MaRDI portal
Recommendations
Cited in
(66)- A general method of axiomatizing fragments
- The effects of adding reachability predicates in propositional separation logic
- Compositional entailment checking for a fragment of separation logic
- Unifying separation logic and region logic to allow interoperability
- A separation logic with data: small models and automation
- A decision procedure for separation logic in SMT
- Contributed papers. Restriction on cut in cyclic proof system for symbolic heaps
- A decidable fragment in separation logic with inductive predicates and arithmetic
- Strong-separation logic
- Compositional satisfiability solving in separation logic
- Extended transitive separation logic
- Decidability of the monadic shallow linear first-order fragment with straight dismatching constraints
- Automated mutual induction proof in separation logic
- A logic of reachable patterns in linked data-structures
- Compositional entailment checking for a fragment of separation logic
- Decision procedures for region logic
- Transitive Separation Logic
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
- Unified reasoning about robustness properties of symbolic-heap separation logic
- Tractable Reasoning in a Fragment of Separation Logic
- Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
- A Logic-Based Framework for Reasoning about Composite Data Structures
- Undecidability of propositional separation logic and its neighbours
- Disproving inductive entailments in separation logic via base pair approximation
- Separation logic with monadic inductive definitions and implicit existentials
- On the Almighty Wand
- Quantitative Separation Logic and Programs with Lists
- Beyond Shapes: Lists with Ordered Data
- On Model Checking Boolean BI
- On the almighty wand
- Separation logics and modalities: a survey
- The tree width of separation logic with recursive definitions
- Decidability for entailments of symbolic heaps with arrays
- Local reasoning for global graph properties
- A first-order logic with frames
- Decision Procedure for Entailment of Symbolic Heaps with Arrays
- On temporal and separation logics
- Tractability of separation logic with inductive definitions: beyond lists
- On Symbolic Heaps Modulo Permission Theories
- A complete axiomatisation for quantifier-free separation logic
- Decidable fragments of field theories
- Compositional invariant checking for overlaid and nested linked lists
- An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
- From separation logic to first-order logic
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- Automatically verifying temporal properties of pointer programs with cyclic proof
- Verifying pointer safety for programs with unknown calls
- A proof procedure for separation logic with inductive definitions and data
- An undecidability result for separation logic with theory reasoning
- Foundations for entailment checking in quantitative separation logic
- An algebraic glimpse at bunched implications and separation logic
- Make flows small again: revisiting the flow framework
- Completeness of cyclic proofs for symbolic heaps with inductive definitions
- Restriction on cut rule in cyclic-proof system for symbolic heaps
- Representation of Peano arithmetic in separation logic
- A structurally complete fragment of relevant logic
- Expressive completeness of separation logic in block-based cloud storage systems
- Beyond symbolic heaps: deciding separation logic with inductive definitions
- An EXPTIME-complete entailment problem in separation logic
- Quantitative separation logic and programs with lists
- Failure of cut-elimination in cyclic-proof systems of logic of bunched implications with inductive propositions
- Encoding Peano arithmetic in a minimal fragment of separation logic
- A shape graph logic and a shape system
- Juggrnaut: using graph grammars for abstracting unbounded heap structures
- Formal verification of C systems code. Structured types, separation logic and theorem proving
- Resources, concurrency, and local reasoning
This page was built for publication: A decidable fragment of separation logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5465888)
