Compositional satisfiability solving in separation logic

DOI10.1007/978-3-030-67067-2_26MaRDI QIDQ2234106zbMATH OpenOpenAlexFDO

Authors 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

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70)

Recommendations

• A decision procedure for satisfiability in separation logic with inductive predicates
• A decidable fragment in separation logic with inductive predicates and arithmetic
• Satisfiability of compositional separation logic with tree predicates and data constraints
• A complete decision procedure for linearly compositional separation logic with data constraints
• Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic

Cites work

• A complete decision procedure for linearly compositional separation logic with data constraints
• A decidable fragment in separation logic with inductive predicates and arithmetic
• A decision procedure for satisfiability in separation logic with inductive predicates
• A decision procedure for string logic with quadratic equations, regular expressions and length constraints
• A separation logic with data: small models and automation
• BI as an assertion language for mutable data structures
• Bi-Abduction with Pure Properties for Specification Inference
• Biabduction (and related problems) in array separation logic
• Compositional entailment checking for a fragment of separation logic
• Compositional shape analysis by means of bi-abduction
• Computer Aided Verification
• Decidability of the universal theory of natural numbers with addition and divisibility
• Decidable logics combining heap structures and data
• Deciding entailments in inductive separation logic with tree automata
• 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
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Foundations of Software Science and Computational Structures
• Frame inference for inductive entailment proofs in separation logic
• On the complexity of pointer arithmetic in separation logic
• Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
• Satisfiability modulo heap-based programs
• Satisfiability of compositional separation logic with tree predicates and data constraints
• Separation logic modulo theories
• The Bernays-Schönfinkel-Ramsey class of separation logic on arbitrary domains
• The Diophantine Problem for Addition and Divisibility
• Unified reasoning about robustness properties of symbolic-heap separation logic

Cited in

(9)

• Satisfiability of compositional separation logic with tree predicates and data constraints
• Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination
• A proof procedure for separation logic with inductive definitions and data
• Single-domain free logic and the problem of compositionality
• Combining preorder and postorder resolution in a satisfiability solver
• An efficient cyclic entailment procedure in a fragment of separation logic
• Testing the satisfiability of formulas in separation logic with permissions
• Separation logic with linearly compositional inductive predicates and set data constraints
• Separating signs in the propositional satisfiability problem

This page was built for publication: Compositional satisfiability solving in separation logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2234106)