@article{oai:repository.nii.ac.jp:00001259,
 author = {龍田, 真 and Tatsuta, Makoto and Chin, Wei-Ngan and Ameen, Mahmudul Faisal Al},
 journal = {NIIテクニカル・レポート, NII Technical Report},
 month = {Jul},
 note = {Reynolds' separation logical system for pointer program verification is investigated. This paper proves its completeness theorem as well as the expressiveness theorem of Peano arithmetic language for the system under the standard interpretation. 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.},
 pages = {1--14},
 title = {NII Technical Report (NII-2009-013E)：Completeness of Pointer Program Verification by Separation Logic},
 year = {2009}
}