Call Invariants

8 years 1 months ago
Call Invariants
Program verifiers based on first-order theorem provers model the program heap as a collection of mutable maps. In such verifiers, preserving unmodified facts about the heap across procedure calls is difficult because of scoping and modification of possibly unbounded set of heap locations. Existing approaches to deal with this problem are either too imprecise, require introducing untrusted assumptions in the verifier, or resort to unpredictable reasoning using quantifiers. In this work, we propose a new approach to solve this problem. The centerpiece of our approach is the call invariant, a new annotation for procedure calls. A call invariant allows the user to specify at a call site an assertion that is inductively preserved across an arbitrary update to a heap location modified in the call. Our approach allows us to leverage existing techniques for reasoning about call-free programs to precisely and predictably reason about programs with procedure calls. We have implemented th...
Shuvendu K. Lahiri, Shaz Qadeer
Added 14 May 2011
Updated 14 May 2011
Type Journal
Year 2011
Where NFM
Authors Shuvendu K. Lahiri, Shaz Qadeer
Comments (0)