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 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.