A decision procedure for satisfiability in separation logic with inductive predicates

DOI10.1145/2603088.2603091MaRDI QIDQ4635608zbMATH OpenOpenAlexWikidataFDO

Authors James Brotherston, Carsten Fuhs, Nikos Gorogiannis, Juan Antonio Pérez

Publication date 23 April 2018

Published in Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2603088.2603091

zbMATH Keywords

satisfiabilityseparation logicdecision procedureinductive predicates

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70)

Recommendations

• A decidable fragment in separation logic with inductive predicates and arithmetic
• Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
• Model checking for symbolic-heap separation logic with inductive predicates
• Satisfiability modulo heap-based programs
• A decision procedure for separation logic in SMT

Cited in

(28)

• Unified reasoning about robustness properties of symbolic-heap separation logic
• Compositional satisfiability solving in separation logic
• scientific article; zbMATH DE number 7350781 (Why is no real title available?)
• Disproving inductive entailments in separation logic via base pair approximation
• Separation logics and modalities: a survey
• The SAT-based approach to separation logic
• Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination
• Decision Procedure for Entailment of Symbolic Heaps with Arrays
• A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
• On temporal and separation logics
• Decision problems in a logic for reasoning about reconfigurable distributed systems
• Two-Variable Separation Logic and Its Inner Circle
• Foundations for decision problems in separation logic with general inductive predicates
• Tractability of separation logic with inductive definitions: beyond lists
• The Bernays-Schönfinkel-Ramsey class of separation logic with uninterpreted predicates
• Unifying decidable entailments in separation logic with inductive definitions
• A decision procedure for separation logic in SMT
• Decision procedures for region logic
• Separation logic with one quantified variable
• Compositional entailment checking for a fragment of separation logic
• A complete decision procedure for linearly compositional separation logic with data constraints
• Satisfiability modulo heap-based programs
• Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
• SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions
• Completeness of cyclic proofs for symbolic heaps with inductive definitions
• Testing the satisfiability of formulas in separation logic with permissions
• A decidable fragment in separation logic with inductive predicates and arithmetic
• Separation logic with linearly compositional inductive predicates and set data constraints

This page was built for publication: A decision procedure for satisfiability in separation logic with inductive predicates

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