A Decision Procedure for Separation Logic in SMT

The work

AuthorsAndrew Reynolds; Radu Iosif; Cristina Serban; Tim L. King
Editors
Typeinproceedings
Year2016
Citekeyreynolds2016decision

Where it appeared

Published inAutomated Technology for Verification and Analysis
PublisherSpringer
Pages244--261

Identifiers

DOI10.1007/978-3-319-46520-3_16
OpenAlexW2309670657

Access

Landing pagehttps://doi.org/10.1007/978-3-319-46520-3_16
Free full texthttps://hal.science/hal-01418883

Abstract

This paper presents a complete decision procedure for the entire quantifier-free fragment of Separation Logic (SL) interpreted over heaplets with data elements ranging over a parametric multi-sorted (possibly infinite) domain. The algorithm uses a combination of theories and is used as a specialized solver inside a DPLL(T ) architecture. A prototype was implemented within the CVC4 SMT solver. Preliminary evaluation suggests the possibility of using this procedure as a building block of a more elaborate theorem prover for SL with inductive predicates, or as back-end of a bounded model checker for programs with low-level pointer and data manipulations.

A copy is held

pdf, 244.0 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via openalex
Added2026-08-04 00:00 UTC
Approved bya person 2026-08-17 08:36 UTC

Filed under

andrewreynolds atva drheap iosif lncs separation-logic serban the-copy-is-not-the-work

Cite it as

@inproceedings{reynolds2016decision,
  title        = {A Decision Procedure for Separation Logic in SMT},
  author       = {Andrew Reynolds and Radu Iosif and Cristina Serban and Tim L. King},
  year         = {2016},
  booktitle    = {Automated Technology for Verification and Analysis},
  publisher    = {Springer},
  pages        = {244--261},
  doi          = {10.1007/978-3-319-46520-3_16},
}

This record lives at https://refs.drheap.org/reynolds2016decision/ and will keep doing so.