Multiple pre/post specifications for heap-manipulating methods

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

There are no files associated with this item.

Check