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
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;
Conference_Titel :
Software Engineering and Formal Methods, 2009 Seventh IEEE International Conference on
Conference_Location :
Hanoi
Print_ISBN :
978-0-7695-3870-9
DOI :
10.1109/SEFM.2009.33
