Completeness of Pointer Program Verification by Separation Logic

Authors	Makoto Tatsuta; Wei-Ngan Chin; Mahmudul Faisal Al Ameen
Editors
Type	inproceedings
Year	2009
Citekey	`tatsuta2009completeness`

Published in	2009 Seventh IEEE International Conference on Software Engineering and Formal Methods
Publisher	IEEE
Pages	179--188

DOI	10.1109/sefm.2009.33
OpenAlex	W2122066631

Landing page	https://doi.org/10.1109/sefm.2009.33

Reynolds' separation logical system for pointer program verification is investigated. This paper proves its completeness theorem as well as the expressiveness theorem that states the weakest precondition of every program and every assertion can be expressed by some assertion. This paper also introduces the predicate that represents the next new cell, and proves the completeness and the soundness of the extended system under deterministic semantics.

How it got here	agent via crossref
Added	2026-08-07 00:00 UTC
Approved by	a person 2026-08-21 05:51 UTC

alameen chin sefm separation-logic tatsuta

@inproceedings{tatsuta2009completeness,
  title        = {Completeness of Pointer Program Verification by Separation Logic},
  author       = {Makoto Tatsuta and Wei-Ngan Chin and Mahmudul Faisal Al Ameen},
  year         = {2009},
  booktitle    = {2009 Seventh IEEE International Conference on Software Engineering and Formal Methods},
  publisher    = {IEEE},
  pages        = {179--188},
  doi          = {10.1109/sefm.2009.33},
}

This record lives at https://refs.drheap.org/tatsuta2009completeness/ and will keep doing so.

Completeness of Pointer Program Verification by Separation Logic

The work

Where it appeared

Identifiers

Access

Abstract

How it got here

Filed under

Cite it as