Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/39887
Title: Completeness of Pointer Program Verification by Separation Logic
Authors: Tatsuta, M.
Chin, W.-N. 
Al Ameen, M.F.
Issue Date: 2009
Source: Tatsuta, M.,Chin, W.-N.,Al Ameen, M.F. (2009). Completeness of Pointer Program Verification by Separation Logic. NII Technical Reports (13) : 1-15. ScholarBank@NUS Repository.
Abstract: 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.
Source Title: NII Technical Reports
URI: http://scholarbank.nus.edu.sg/handle/10635/39887
ISSN: 13465597
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

Page view(s)

77
checked on Dec 8, 2017

Google ScholarTM

Check


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.