Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic

DOI10.1007/978-3-319-52234-0_25MaRDI QIDQ2961583zbMATH OpenOpenAlexFDO

Authors Andrew Reynolds, Radu Iosif, C. Şerban

Publication date 21 February 2017

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1610.04707

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Abstract: Separation Logic (SL) is a well-known assertion language used in Hoare-style modular proof systems for programs with dynamically allocated data structures. In this paper we investigate the fragment of first-order SL restricted to the Bernays-Schoenfinkel-Ramsey quantifier prefix $exist{s}^{\ast }foral{l}^{\ast }$, where the quantified variables range over the set of memory locations. When this set is uninterpreted (has no associated theory) the fragment is PSPACE-complete, which matches the complexity of the quantifier-free fragment. However, SL becomes undecidable when the quantifier prefix belongs to $exist{s}^{\ast }foral{l}^{\ast }exist{s}^{\ast }$ instead, or when the memory locations are interpreted as integers with linear arithmetic constraints, thus setting a sharp boundary for decidability within SL. We have implemented a decision procedure for the decidable fragment of $exist{s}^{\ast }foral{l}^{\ast }$SL as a specialized solver inside a DPLL($T$) architecture, within the CVC4 SMT solver. The evaluation of our implementation was carried out using two sets of verification conditions, produced by (i) unfolding inductive predicates, and (ii) a weakest precondition-based verification condition generator. Experimental data shows that automated quantifier instantiation has little overhead, compared to manual model-based instantiation.

Recommendations

• Tractable Reasoning in a Fragment of Separation Logic
• The Bernays-Schönfinkel-Ramsey class of separation logic on arbitrary domains
• The Bernays-Schönfinkel-Ramsey class of separation logic with uninterpreted predicates
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• An undecidability result for separation logic with theory reasoning
• Separation logic style reasoning in a refinement based language
• Splittings in varieties of logic
• Compositional entailment checking for a fragment of separation logic
• Compositional entailment checking for a fragment of separation logic
• The complexity of reasoning for fragments of default logic

Cites work

• scientific article; zbMATH DE number 2081098 (Why is no real title available?)
• scientific article; zbMATH DE number 3336816 (Why is no real title available?)
• A decision procedure for separation logic in SMT
• BI as an assertion language for mutable data structures
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Complexity results for classes of quantificational formulas
• Computer Aided Verification
• Counterexample-guided quantifier instantiation for synthesis in SMT
• Deciding effectively propositional logic using DPLL and substitution sets
• Enhancing Program Verification with Lemmas
• On the almighty wand
• Presburger arithmetic with unary predicates is Π₁¹ complete
• Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
• Separation logic with one quantified variable
• Sequent calculi for induction and infinite descent
• Spatial interpolants
• Tableaux and resource graphs for separation logic
• Two-Variable Separation Logic and Its Inner Circle
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)

Cited in

(12)

• Compositional satisfiability solving in separation logic
• The Bernays-Schönfinkel-Ramsey class of separation logic on arbitrary domains
• Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
• Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
• Separation logic and logics with team semantics
• Program Verification with Separation Logic
• The Bernays-Schönfinkel-Ramsey class of separation logic with uninterpreted predicates
• Prenex separation logic with one selector field
• Tractable Reasoning in a Fragment of Separation Logic
• A reason maintenance perspective on relevant Ramsey conditionals
• Strong-separation logic
• Quantitative Separation Logic and Programs with Lists

Describes a project that uses

Uses Software

• Infer
• iProver
• CVC4
• Predator

This page was built for publication: Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic

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