Completeness of separation logic with inductive definitions for program verification
The work
| Authors | Makoto Tatsuta; Wei-Ngan Chin |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2014 |
| Citekey | tatsuta2014completeness |
Where it appeared
| Published in | International Conference on Software Engineering and Formal Methods |
|---|---|
| Publisher | Springer |
| Series | Lecture Notes in Computer Science |
| Number in series | 8702 |
| Pages | 20--34 |
Identifiers
| DOI | 10.1007/978-3-319-10431-7_3 |
|---|
Abstract
This paper extends Reynolds’ separation logical system for pointer-based while program verification by adding inductive definitions. Inductive definitions give us a great advantage for verification, since they enable us for example, to formalize linked lists and to support the lemma reasoning mechanism. This paper proves its completeness theorem that states that every true asserted program is provable in the logical system. In order to prove its completeness, this paper shows an expressiveness theorem that states the weakest precondition of every program and every assertion can be expressed by some assertion.
A copy is held
pdf, 242.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-16 15:30 UTC |
Filed under
Cite it as
@inproceedings{tatsuta2014completeness,
title = {Completeness of separation logic with inductive definitions for program verification},
author = {Makoto Tatsuta and Wei-Ngan Chin},
year = {2014},
booktitle = {International Conference on Software Engineering and Formal Methods},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
pages = {20--34},
doi = {10.1007/978-3-319-10431-7_3},
}
This record lives at https://refs.drheap.org/tatsuta2014completeness/ and will keep doing so.