Paper Info
Title
Verifying heap-manipulating programs with unknown procedure calls
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 mspecu 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 mspecu. The expected specification mspecu 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.
Year
DOI
Venue
2010
10.1007/978-3-642-16901-4_13
ICFEM
Keywords
Field
DocType
program prog,verifying prog,unknown call,procedure unknown,specification mspecu,practical problem,unknown procedure,unknown procedure unknown,hoare-style specification,heap-manipulating program,expected specification mspecu,unknown procedure call,data structure,shape analysis
Pointer (computer programming),Data structure,Separation logic,Programming language,Computer science,Unknown procedure,Correctness,Heap (data structure),Theoretical computer science,Symbolic execution,Shape analysis (digital geometry)
Conference
Volume
ISSN
ISBN
6447
0302-9743
3-642-16900-7
Citations 
PageRank 
References 
0
0.34
15
Authors
5
Name
Order
Citations
PageRank
Shengchao Qin171162.81
Chenguang Luo2565.63
Guanhua He3687.50
Florin Craciun4408.19
Wei-Ngan Chin586863.37