Multiple pre/post specifications for heap-manipulating methods

Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, Shengchao Qin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

128 Downloads (Pure)


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.
Original languageEnglish
Title of host publication10th IEEE High Assurance Systems Engineering Symposium (HASE'07)
ISBN (Print)9780769530437
Publication statusPublished - 2007
EventIEEE High Assurance Systems Engineering Symposium - Dallas, Texas, United States
Duration: 14 Nov 200716 Nov 2007
Conference number: 10


ConferenceIEEE High Assurance Systems Engineering Symposium
Abbreviated titleHASE'07
Country/TerritoryUnited States

Bibliographical note

Author can archive publisher's version/PDF.


Dive into the research topics of 'Multiple pre/post specifications for heap-manipulating methods'. Together they form a unique fingerprint.

Cite this