Sciweavers

Share
ICFEM
2010
Springer

Verifying Heap-Manipulating Programs with Unknown Procedure Calls

10 years 10 months ago
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 specifisigned for a combined abstract domain. We have also done some experiment...
Shengchao Qin, Chenguang Luo, Guanhua He, Florin C
Added 26 Jan 2011
Updated 26 Jan 2011
Type Journal
Year 2010
Where ICFEM
Authors Shengchao Qin, Chenguang Luo, Guanhua He, Florin Craciun, Wei-Ngan Chin
Comments (0)
books