Multiple Pre/Post Specifications for Heap-Manipulating Methods

Chin, W.N.; David, C.; Nguyen, H.H.; Qin, S.

doi:10.1109/hase.2007.19

Multiple Pre/Post Specifications for Heap-Manipulating Methods

Chin, W.N.; David, C.; Nguyen, H.H.; Qin, S.

Authors

W.N. Chin

C. David

H.H. Nguyen

S. Qin

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.

Citation

Chin, W., David, C., Nguyen, H., & 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. (357-364). https://doi.org/10.1109/hase.2007.19

Conference Name	10th IEEE High Assurance Systems Engineering Symposium (HASE 2007)
Conference Location	Dallas, Texas, USA
Start Date	Nov 14, 2007
End Date	Nov 16, 2007
Publication Date	Nov 1, 2007
Deposit Date	Nov 17, 2009
Publicly Available Date	Nov 17, 2009
Publisher	Institute of Electrical and Electronics Engineers
Pages	357-364
Book Title	IEEE International Symposium on High Assurance Systems Engineering : 14-16 November 2007, Dallas, Texas ; proceedings..
ISBN	07695304352
DOI	https://doi.org/10.1109/hase.2007.19

Files

Published Conference Proceeding (109 Kb)
PDF

Copyright 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.