Chin, W.-N. and David, C. and Nguyen, H. H. and Qin, S. (2007) 'Multiple pre/post specifications for heap-manipulating methods.', in IEEE International Symposium on High Assurance Systems Engineering : 14-16 November 2007, Dallas, Texas ; proceedings.. Los Alamitos, CA: IEEE, pp. 357-364.
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.
|Item Type:||Book chapter|
|Full text:||(VoR) Version of Record|
Download PDF (107Kb)
|Publisher Web site:||http://dx.doi.org/10.1109/HASE.2007.19|
|Publisher statement:||© 2007 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.|
|Record Created:||17 Nov 2009 12:05|
|Last Modified:||08 Nov 2010 12:27|
|Social bookmarking:||Export: EndNote, Zotero | BibTex|
|Look up in GoogleScholar | Find in a UK Library|