Please use this identifier to cite or link to this item:
Title: Multiple pre/post specifications for heap-manipulating methods
Authors: Chin, W.-N. 
David, C.
Nguyen, H.H.
Qin, S.
Issue Date: 2007
Citation: Chin, W.-N., David, C., Nguyen, H.H., Qin, S. (2007). Multiple pre/post specifications for heap-manipulating methods. Proceedings of IEEE International Symposium on High Assurance Systems Engineering : 357-364. ScholarBank@NUS Repository.
Abstract: Automated verification plays an important role for high assurance software. This typically uses a pair of pre/post conditions as a formal (but possibly partial) specification of each method before it is systematically verified. In this paper, we advocate for multiple pairs of pre/post conditions to be associated with each method which provides a way for such specification to be used in more scenarios. Multiple pre/post specifications are important for heap-manipulating programs where they can be precisely expressed using separation logic. This work highlights the importance of multiple pre/post specifications, and a methodology to capture them via set of states during proof search. © 2007 IEEE.
Source Title: Proceedings of IEEE International Symposium on High Assurance Systems Engineering
ISBN: 0769530435
ISSN: 15302059
DOI: 10.1109/HASE.2007.56
Appears in Collections:Staff Publications

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


checked on Mar 23, 2019

Page view(s)

checked on Mar 3, 2019

Google ScholarTM



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