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)

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