2024-03-28T12:58:36Z
https://repository.nii.ac.jp/oai
oai:repository.nii.ac.jp:00001259
2023-01-06T08:33:15Z
136
NII Technical Report (NII-2009-013E):Completeness of Pointer Program Verification by Separation Logic
龍田, 真
Tatsuta, Makoto
Chin, Wei-Ngan
Ameen, Mahmudul Faisal Al
テクニカルレポート
Technical Report
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.
国立情報学研究所
2009-07-09
eng
departmental bulletin paper
https://doi.org/10.20736/0000001259
https://repository.nii.ac.jp/records/1259
10.20736/0000001259
1346-5597
NIIテクニカル・レポート
NII Technical Report
1
14
https://repository.nii.ac.jp/record/1259/files/09-013E.pdf
application/pdf
253.4 kB
2019-03-12