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

DOI10.1007/978-3-319-52234-0_25zbMath1484.68104arXiv1610.04707OpenAlexW2537376148MaRDI QIDQ2961583

Andrew Reynolds, Radu Iosif, Cristina Serban

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

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

Related Items (6)

Program Verification with Separation Logic ⋮ Separation logic and logics with team semantics ⋮ Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic ⋮ Strong-separation logic ⋮ Compositional satisfiability solving in separation logic ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates

Uses Software

• Predator
• CVC4
• iProver
• Infer

Cites Work

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

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