Compositional satisfiability solving in separation logic
From MaRDI portal
Publication:2234106
DOI10.1007/978-3-030-67067-2_26zbMath1472.03025OpenAlexW3119321758MaRDI QIDQ2234106
Publication date: 18 October 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-67067-2_26
Logic in computer science (03B70) Decidability of theories and sets of sentences (03B25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Related Items
A proof procedure for separation logic with inductive definitions and data ⋮ An efficient cyclic entailment procedure in a fragment of separation logic
Cites Work
- Decidability of the universal theory of natural numbers with addition and divisibility
- Compositional entailment checking for a fragment of separation logic
- A separation logic with data: small models and automation
- A decidable fragment in separation logic with inductive predicates and arithmetic
- The Bernays-Schönfinkel-Ramsey class of separation logic on arbitrary domains
- Frame inference for inductive entailment proofs in separation logic
- Biabduction (and related problems) in array separation logic
- Satisfiability of compositional separation logic with tree predicates and data constraints
- A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints
- Separation Logic Modulo Theories
- Bi-Abduction with Pure Properties for Specification Inference
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
- Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic
- Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
- Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation
- Deciding Entailments in Inductive Separation Logic with Tree Automata
- The Diophantine Problem for Addition and Divisibility
- Satisfiability Modulo Heap-Based Programs
- A decision procedure for satisfiability in separation logic with inductive predicates
- BI as an assertion language for mutable data structures
- Compositional Shape Analysis by Means of Bi-Abduction
- Decidable logics combining heap structures and data
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Foundations of Software Science and Computational Structures
- Computer Aided Verification
- On the complexity of pointer arithmetic in separation logic
- A decision procedure for string logic with quadratic equations, regular expressions and length constraints
This page was built for publication: Compositional satisfiability solving in separation logic