A decidable fragment in separation logic with inductive predicates and arithmetic

DOI10.1007/978-3-319-63390-9_26MaRDI QIDQ2164251zbMATH OpenOpenAlexFDO

Authors Quang Loc Le, Makoto Tatsuta, Jun Sun, Wei-Ngan Chin

Publication date 12 August 2022

Full work available at URL https://ink.library.smu.edu.sg/sis_research/4702

zbMATH Keywords

decidabilityinductive predicatessatisfiability solvingseparation logic

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• A decision procedure for satisfiability in separation logic with inductive predicates
• Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Satisfiability modulo heap-based programs
• A decision procedure for separation logic in SMT

Cited in

(16)

• Reasoning about block-based cloud storage systems via separation logic
• Strong-separation logic
• Compositional satisfiability solving in separation logic
• Tractable Reasoning in a Fragment of 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
• Satisfiability modulo heap-based programs
• A decision procedure for satisfiability in separation logic with inductive predicates
• Extending propositional separation logic for robustness properties
• The Bernays-Schönfinkel-Ramsey class of separation logic with uninterpreted predicates
• Foundations for decision problems in separation logic with general inductive predicates
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
• An efficient cyclic entailment procedure in a fragment of separation logic
• Concolic testing heap-manipulating programs
• Encoding Peano arithmetic in a minimal fragment of separation logic

This page was built for publication: A decidable fragment in separation logic with inductive predicates and arithmetic

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