We use cookies to ensure that we give you the best experience on our website. By continuing to browse this repository, you give consent for essential cookies to be used. You can read more about our Privacy and Cookie Policy.

Durham Research Online
You are in:

Multiple pre/post specifications for heap-manipulating methods.

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
Publisher Web site:
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: del.icio.usConnoteaBibSonomyCiteULikeFacebookTwitterExport: EndNote, Zotero | BibTex
Look up in GoogleScholar | Find in a UK Library