1. ScholarBank@NUS
  2. 1. Staff
  3. Staff Publications
Please use this identifier to cite or link to this item: https://doi.org/10.1109/SEFM.2009.33
DC FieldValue
dc.titleCompleteness of pointer program verification by separation logic
dc.contributor.authorTatsuta, M.
dc.contributor.authorChin, W.-N.
dc.contributor.authorAl Ameen, M.F.
dc.date.accessioned2013-07-04T08:08:53Z
dc.date.available2013-07-04T08:08:53Z
dc.date.issued2009
dc.identifier.citationTatsuta, 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
dc.identifier.isbn9780769538709
dc.identifier.urihttp://scholarbank.nus.edu.sg/handle/10635/40636
dc.description.abstractReynolds' 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.
dc.description.urihttp://libproxy1.nus.edu.sg/login?url=http://dx.doi.org/10.1109/SEFM.2009.33
dc.sourceScopus
dc.typeConference Paper
dc.contributor.departmentCOMPUTER SCIENCE
dc.description.doi10.1109/SEFM.2009.33
dc.description.sourcetitleSEFM 2009 - 7th IEEE International Conference on Software Engineering and Formal Methods
dc.description.page179-188
dc.identifier.isiut000275404000018
Appears in Collections:Staff Publications

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

Google ScholarTM

Check

Altmetric


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