DocumentCode
2893903
Title
Completeness of Pointer Program Verification by Separation Logic
Author
Tatsuta, Makoto ; Chin, Wei-Ngan ; Ameen, Mohammad
Author_Institution
Nat. Inst. of Inf., Tokyo, Japan
fYear
2009
fDate
23-27 Nov. 2009
Firstpage
179
Lastpage
188
Abstract
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.
Keywords
formal logic; program verification; Reynolds separation logical system; completeness theorem; deterministic semantics; pointer program verification; Arithmetic; Automatic logic units; Computer languages; Computer science; Informatics; Pathology; Software engineering; completeness theorem; expressiveness theorem; pointer program verification; separation logic;
fLanguage
English
Publisher
ieee
Conference_Titel
Software Engineering and Formal Methods, 2009 Seventh IEEE International Conference on
Conference_Location
Hanoi
Print_ISBN
978-0-7695-3870-9
Type
conf
DOI
10.1109/SEFM.2009.33
Filename
5368097
Link To Document