Completeness of pointer program verification by separation logic

Please use this identifier to cite or link to this item: https://doi.org/10.1109/SEFM.2009.33

Title:	Completeness of pointer program verification by separation logic
Authors:	Tatsuta, M. Chin, W.-N. Al Ameen, M.F.
Issue Date:	2009
Citation:	Tatsuta, M., Chin, W.-N., Al Ameen, M.F. (2009). Completeness of pointer program verification by separation logic. SEFM 2009 - 7th IEEE International Conference on Software Engineering and Formal Methods : 179-188. ScholarBank@NUS Repository. https://doi.org/10.1109/SEFM.2009.33
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. © 2009 IEEE.
Source Title:	SEFM 2009 - 7th IEEE International Conference on Software Engineering and Formal Methods
URI:	http://scholarbank.nus.edu.sg/handle/10635/40636
ISBN:	9780769538709
DOI:	10.1109/SEFM.2009.33
Appears in Collections:	Staff Publications

There are no files associated with this item.

Check