Completeness for recursive procedures in separation logic
The work
| Title | Completeness for recursive procedures in separation logic |
|---|---|
| Authors | Mahmudul Faisal Al Ameen; Makoto Tatsuta |
| Type | article |
| Year | 2016 |
| Citekey | ameen2016completeness |
Where it appeared
| Published in | Theoretical Computer Science |
|---|---|
| Publisher | Elsevier |
| Volume | 631 |
| Pages | 73--96 |
Identifiers
| DOI | 10.1016/j.tcs.2016.04.004 |
|---|
Access
| Landing page | https://www.sciencedirect.com/science/article/pii/S0304397516300329 |
|---|
Abstract
This paper proves the completeness of an extension of Hoare's logic and separation logic for pointer programs with mutual recursive procedures. This paper shows the expressiveness of the assertion language as well. This paper achieves a new system by introducing two new inference rules, and removes an axiom that is unsound in separation logic and other redundant inference rules for showing completeness. It introduces a novel expression that is used to describe complete information of a given state in a precondition. This work also uses the necessary and sufficient precondition of a program for the abort-free execution, which enables us to utilize strongest postconditions.
Copy held
| Kind | PDF, 786.2 kB |
|---|---|
| Retrieved | 2026-08-10 |
| Held | local, for personal reference |
| Where it came from | https://www.sciencedirect.com/science/article/pii/S0304397516300329 |
Where this came from
| How it got here | the agent went looking · found via bibtex |
|---|---|
| First seen | 2026-08-05 |
| Record | reviewed by a person |
| Approved | 2026-08-10 |
Cite it as
@article{ameen2016completeness,
title = {Completeness for recursive procedures in separation logic},
author = {Mahmudul Faisal Al Ameen and Makoto Tatsuta},
year = {2016},
journal = {Theoretical Computer Science},
volume = {631},
pages = {73--96},
publisher = {Elsevier},
doi = {10.1016/j.tcs.2016.04.004},
url = {https://www.sciencedirect.com/science/article/pii/S0304397516300329},
}
This record lives at https://refs.drheap.org/ameen2016completeness/ and will keep doing so.