Completeness for recursive procedures in separation logic
The work
| Authors | Mahmudul Faisal Al Ameen; Makoto Tatsuta |
|---|---|
| Editors | |
| 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 |
|---|
Related
| Distinct from | ameen2016completenessverification |
|---|
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.
A copy is held
pdf, 767.7 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-08-10 21:26 UTC |
Filed under
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},
publisher = {Elsevier},
volume = {631},
pages = {73--96},
doi = {10.1016/j.tcs.2016.04.004},
}
This record lives at https://refs.drheap.org/ameen2016completeness/ and will keep doing so.