Sciweavers

JSC
2010

Verifying pointer safety for programs with unknown calls

13 years 2 months ago
Verifying pointer safety for programs with unknown calls
We study the automated verification of pointer safety for heap-manipulating imperative programs with unknown procedure calls. Given a Hoare-style partial correctness specification S = {Pre} C {Post} in separation logic, where the program C contains calls to some unknown procedure U, we infer a specification SU for the unknown procedure U from the calling contexts. We show that the problem of verifying the program C against the specification S can be safely reduced to the problem of proving that the procedure U (once its code is available) meets the derived specification SU . The expected specification SU for the unknown procedure U is automatically calculated using an abduction-based shape analysis. We have also implemented a prototype system to validate the viability of our approach. Preliminary results show that the specifications derived by our tool fully capture the behaviors of the unknown code in many cases. Key words: Inference, verification, abduction, separation logic...
Chenguang Luo, Florin Craciun, Shengchao Qin, Guan
Added 29 Jan 2011
Updated 29 Jan 2011
Type Journal
Year 2010
Where JSC
Authors Chenguang Luo, Florin Craciun, Shengchao Qin, Guanhua He, Wei-Ngan Chin
Comments (0)