Separation logic modulo theories

DOI10.1007/978-3-319-03542-0_7MaRDI QIDQ2937786zbMATH OpenOpenAlexFDO

Authors Andrey Rybalchenko, Juan Antonio Pérez

Publication date 12 January 2015

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

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

Mathematics Subject Classification ID

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

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.

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

Cited in

(24)

• Unified reasoning about robustness properties of symbolic-heap separation logic
• 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
• A logic of separating modalities
• Horn clause solvers for program verification
• Lightweight Separation
• 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
• Compositional entailment checking for a fragment of separation logic
• An efficient cyclic entailment procedure in 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
• Enhancing Program Verification with Lemmas
• Completeness of cyclic proofs for symbolic heaps with inductive definitions
• Testing the satisfiability of formulas in separation logic with permissions
• Transitive 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)