Separation logic modulo theories

DOI10.1007/978-3-319-03542-0_7zbMATH Open1426.68058arXiv1303.2489OpenAlexW1841862047MaRDI QIDQ2937786FDOQ2937786

Authors: Andrey Rybalchenko, Juan Antonio Pérez 

Publication date: 12 January 2015

Published in: Programming Languages and Systems (Search for Journal in Brave)

Abstract: Logical reasoning about program data often requires dealing with heap structures as well as scalar data types. Recent advances in Satisfiability Modular Theory (SMT) already offer efficient procedures for dealing with scalars, yet they lack any support for dealing with heap structures. In this paper, we present an approach that integrates Separation Logic---a prominent logic for reasoning about list segments on the heap---and SMT. We follow a model-based approach that communicates aliasing among heap cells between the SMT solver and the Separation Logic reasoning part. An experimental evaluation using the Z3 solver indicates that our approach can effectively put to work the advances in SMT for dealing with heap structures. This is the first decision procedure for the combination of separation logic with SMT theories.

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

Recommendations

• Program Verification with Separation Logic
• Satisfiability modulo heap-based programs
• Separation Logic for Higher-Order Store
• A decision procedure for separation logic in SMT
• Computer Science Logic

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Cited In (24)

• Automated theorem proving for assertions in separation logic with all connectives
• Compositional satisfiability solving in separation logic
• Reasoning About Data-Parallel Pointer Programs in a Modal Extension of Separation Logic
• Separation logics and modalities: a survey
• Horn clause solvers for program verification
• Lightweight Separation
• A logic of separating modalities
• A proof procedure for separation logic with inductive definitions and data
• Expressive completeness of separation logic with two variables and no separating conjunction
• Unifying separation logic and region logic to allow interoperability
• Back to the future, revisiting precise program verification using SMT solvers
• Survey of research on program verification via separation logic
• Automated mutual induction proof in separation logic
• Separation logic with one quantified variable
• An efficient cyclic entailment procedure in a fragment of separation logic
• Compositional entailment checking for a fragment of separation logic
• Strong-separation logic
• A first-order logic with frames
• Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
• Completeness of cyclic proofs for symbolic heaps with inductive definitions
• Testing the satisfiability of formulas in separation logic with permissions
• Enhancing Program Verification with Lemmas
• Transitive Separation Logic
• Unified reasoning about robustness properties of symbolic-heap separation logic

This page was built for publication: Separation logic modulo theories

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