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

DOI10.1007/978-3-319-52234-0_25zbMATH Open1484.68104arXiv1610.04707OpenAlexW2537376148MaRDI QIDQ2961583FDOQ2961583

Authors: Andrew Reynolds, Radu Iosif, C. Şerban 

Publication date: 21 February 2017

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

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.

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

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (11)

• Compositional satisfiability solving in separation logic
• 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

Uses Software

• Predator
• CVC4
• iProver
• Infer

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)