Please use this identifier to cite or link to this item: https://doi.org/10.1016/j.jsc.2010.06.003
Title: Verifying pointer safety for programs with unknown calls
Authors: Luo, C.
Craciun, F.
Qin, S.
He, G.
Chin, W.-N. 
Keywords: Abduction
Inference
Separation logic
Verification
Issue Date: 2010
Source: Luo, C., Craciun, F., Qin, S., He, G., Chin, W.-N. (2010). Verifying pointer safety for programs with unknown calls. Journal of Symbolic Computation 45 (11) : 1163-1183. ScholarBank@NUS Repository. https://doi.org/10.1016/j.jsc.2010.06.003
Abstract: 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. © 2010 Elsevier Ltd.
Source Title: Journal of Symbolic Computation
URI: http://scholarbank.nus.edu.sg/handle/10635/39804
ISSN: 07477171
DOI: 10.1016/j.jsc.2010.06.003
Appears in Collections:Staff Publications

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

SCOPUSTM   
Citations

6
checked on Dec 11, 2017

WEB OF SCIENCETM
Citations

4
checked on Dec 11, 2017

Page view(s)

52
checked on Dec 9, 2017

Google ScholarTM

Check

Altmetric


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