Compositional satisfiability solving in separation logic

DOI10.1007/978-3-030-67067-2_26zbMath1472.03025OpenAlexW3119321758MaRDI QIDQ2234106

Quang Loc Le

Publication date: 18 October 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-67067-2_26

zbMATH Keywords

satisfiabilityseparation logicregular proofs

Mathematics Subject Classification ID

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