A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic
The work
| Title | A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic |
|---|---|
| Authors | Quang Loc Le; Makoto Tatsuta; Jun Sun; Wei-Ngan Chin |
| Type | conference paper |
| Year | 2017 |
| Citekey | le2017decidable |
Where it appeared
| Published in | Computer Aided Verification |
|---|---|
| Publisher | Springer |
| Pages | 495--517 |
Identifiers
| DOI | 10.1007/978-3-319-63390-9_26 |
|---|---|
| OpenAlex | W2613252377 |
Access
| Landing page | https://doi.org/10.1007/978-3-319-63390-9_26 |
|---|---|
| Free full text | https://ink.library.smu.edu.sg/sis_research/4702 |
Abstract
We consider the satisfiability problem for a fragment of separation logic including inductive predicates with shape and arithmetic properties. We show that the fragment is decidable if the arithmetic properties can be represented as semilinear sets. Our decision procedure is based on a novel algorithm to infer a finite representation for each inductive predicate which precisely characterises its satisfiability. Our analysis shows that the proposed algorithm runs in exponential time in the worst case. We have implemented our decision procedure and integrated it into an existing verification system. Our experiment on benchmarks shows that our procedure helps to verify the benchmarks effectively.
Copy held
| Kind | PDF, 537.0 kB |
|---|---|
| Retrieved | 2026-08-10 |
| Held | local, for personal reference |
| Where it came from | https://link.springer.com/content/pdf/10.1007/978-3-319-63390-9_26.pdf?error=cookies_not_supported&code=7f97cad2-fd88-4c4f-a82c-8c52f3017fc5 |
Where this came from
| How it got here | the agent went looking · found via openalex |
|---|---|
| First seen | 2026-08-05 |
| Record | reviewed by a person |
| Approved | 2026-08-16 |
Cite it as
@inproceedings{le2017decidable,
title = {A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic},
author = {Quang Loc Le and Makoto Tatsuta and Jun Sun and Wei-Ngan Chin},
year = {2017},
booktitle = {Computer Aided Verification},
pages = {495--517},
publisher = {Springer},
doi = {10.1007/978-3-319-63390-9_26},
url = {https://ink.library.smu.edu.sg/sis_research/4702},
}
This record lives at https://refs.drheap.org/le2017decidable/ and will keep doing so.