Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-21437-0_29
Title: Structured specifications for better verification of heap-manipulating programs
Authors: Gherghina, C.
David, C.
Qin, S.
Chin, W.-N. 
Issue Date: 2011
Citation: Gherghina, C.,David, C.,Qin, S.,Chin, W.-N. (2011). Structured specifications for better verification of heap-manipulating programs. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 6664 LNCS : 386-401. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-21437-0_29
Abstract: Conventional specifications typically have a flat structure that is based primarily on the underlying logic. Such specifications lack structures that could have provided better guidance to the verification process. In this work, we propose to add three new structures to a specification framework for separation logic to achieve a more precise and better guided verification for pointer-based programs. The newly introduced structures empower users with more control over the verification process in the following ways: (i) case analysis can be invoked to take advantage of disjointness conditions in the logic. (ii) early, as opposed to late, instantiation can minimise on the use of existential quantification. (iii) formulae that are staged provide better reuse of the verification process. Initial experiments have shown that structured specifications can lead to more precise verification without incurring any performance overhead. © 2011 Springer-Verlag.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/42002
ISBN: 9783642214363
ISSN: 03029743
DOI: 10.1007/978-3-642-21437-0_29
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.