A Decision Procedure for Separation Logic in SMT
The work
| Title | A Decision Procedure for Separation Logic in SMT |
|---|---|
| Authors | Andrew Reynolds; Radu Iosif; Cristina Serban; Tim L. King |
| Type | conference paper |
| Year | 2016 |
| Citekey | reynolds2016decision |
Where it appeared
| Published in | Automated Technology for Verification and Analysis |
|---|---|
| Publisher | Springer |
| Pages | 244--261 |
Identifiers
| DOI | 10.1007/978-3-319-46520-3_16 |
|---|---|
| OpenAlex | W2309670657 |
Access
| Landing page | https://doi.org/10.1007/978-3-319-46520-3_16 |
|---|---|
| Free full text | https://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.
Copy held
| Kind | PDF, 249.9 kB |
|---|---|
| Retrieved | 2026-08-08 |
| Held | local, for personal reference |
| Opens at | page 2 |
| Where it came from | https://hal.science/hal-01418883/document |
Where this came from
| How it got here | the agent went looking · found via openalex |
|---|---|
| First seen | 2026-08-04 |
| Record | reviewed by a person |
| Approved | 2026-08-17 |
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},
pages = {244--261},
publisher = {Springer},
doi = {10.1007/978-3-319-46520-3_16},
url = {https://hal.science/hal-01418883},
}
This record lives at https://refs.drheap.org/reynolds2016decision/ and will keep doing so.