Please use this identifier to cite or link to this item: https://doi.org/10.1109/HASE.2007.56
Title: Multiple pre/post specifications for heap-manipulating methods
Authors: Chin, W.-N. 
David, C.
Nguyen, H.H.
Qin, S.
Issue Date: 2007
Source: 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. https://doi.org/10.1109/HASE.2007.56
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
URI: http://scholarbank.nus.edu.sg/handle/10635/40427
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.

SCOPUSTM   
Citations

5
checked on Dec 6, 2017

Page view(s)

45
checked on Dec 10, 2017

Google ScholarTM

Check

Altmetric


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