Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-16901-4_13
Title: Verifying heap-manipulating programs with unknown procedure calls
Authors: Qin, S.
Luo, C.
He, G.
Craciun, F.
Chin, W.-N. 
Issue Date: 2010
Source: Qin, S.,Luo, C.,He, G.,Craciun, F.,Chin, W.-N. (2010). Verifying heap-manipulating programs with unknown procedure calls. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 6447 LNCS : 171-187. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-16901-4_13
Abstract: Verification of programs with invocations to unknown procedures is a practical problem, because in many scenarios not all codes of programs to be verified are available. Those unknown calls also pose a challenge for their verification. This paper addresses this problem with an attempt to verify the full functional correctness of such programs using pointer-based data structures. Provided with a Hoare-style specification {Φ pr } prog {Φ po } where program prog contains calls to some unknown procedure unknown, we infer a specification mspec u for unknown from the calling contexts, such that the problem of verifying prog can be safely reduced to the problem of proving that the procedure unknown (once its code is available) meets the derived specification mspec u . The expected specification mspec u for the unknown procedure unknown is automatically calculated using an abduction-based shape analysis specifically designed for a combined abstract domain. We have also done some experiments to validate the viability of our approach. © 2010 Springer-Verlag Berlin Heidelberg.
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/42072
ISBN: 3642169007
ISSN: 03029743
DOI: 10.1007/978-3-642-16901-4_13
Appears in Collections:Staff Publications

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

Page view(s)

70
checked on Dec 16, 2017

Google ScholarTM

Check

Altmetric


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