Please use this identifier to cite or link to this item:
|Title:||Multiple pre/post specifications for heap-manipulating methods|
|Authors:||Chin, W.-N. |
|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|
|Appears in Collections:||Staff Publications|
Show full item record
Files in This Item:
There are no files associated with this item.
checked on Dec 12, 2018
checked on Dec 16, 2018
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.