The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Completeness and expressiveness of pointer program verification by separation logic
The work
| Authors | Makoto Tatsuta; Wei-Ngan Chin; Mahmudul Faisal Al Ameen |
|---|---|
| Editors | |
| Type | article |
| Year | 2019 |
| Citekey | tatsuta2019completenessexpressiveness |
Where it appeared
| Published in | Information and Computation |
|---|---|
| Publisher | Elsevier |
| Volume | 267 |
| Pages | 1--27 |
Identifiers
| DOI | 10.1016/j.ic.2019.03.002 |
|---|
Access
| Landing page | https://www.sciencedirect.com/science/article/pii/S0890540119300203 |
|---|
Empty on purpose
| copy |
Related
| Distinct from | tatsuta2009completeness |
|---|
Abstract
Reynolds' separation logical system for pointer program verification is investigated. This paper proves its completeness theorem that states that every true asserted program is provable in the logical system. In order to prove the completeness, this paper shows the expressiveness theorem that states the weakest precondition of every program and every assertion can be expressed by some assertion. This paper also introduces an extension of the assertion language with inductive definitions and proves the soundness theorem, the expressiveness theorem, and the completeness theorem.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@article{tatsuta2019completenessexpressiveness,
title = {Completeness and expressiveness of pointer program verification by separation logic},
author = {Makoto Tatsuta and Wei-Ngan Chin and Mahmudul Faisal Al Ameen},
year = {2019},
journal = {Information and Computation},
publisher = {Elsevier},
volume = {267},
pages = {1--27},
doi = {10.1016/j.ic.2019.03.002},
}
This record lives at https://refs.drheap.org/tatsuta2019completenessexpressiveness/ and will keep doing so.