VeriFast: Imperative Programs as Proofs
Bart Jacobs, Jan Smans, Frank Piessens · Lirias · 2010
Abstract. We propose an approach for the verification of imperative programs based on the tool-supported, interactive insertion of annotations into the source code. Annotations include routine preconditions and postconditions and loop invariants in a form of separation logic, as well as inductive datatype definitions and recursive function and predicate definitions to enable rich specifications. To enable verification of these rich specifications, annotations also include lemma routines, which are like ordinary routines of the programming language, except that it is checked that they do not have side-effects and that they terminate. Recursive lemma routines serve as inductive proofs that their precondition implies their postcondition. Verification proceeds by symbolic execution, using a separation logicbased representation of memory, and using first-order terms constrained by a first-order theory as symbolic data values. Data value queries are delegated to an SMT solver; since memory framing issues are eliminated from these queries and only well-behaved quantification is used, SMT solver queries perform much better than in verification condition based approaches. Annotation insertion is supported by an integrated development environment where the user may invoke the verification tool. If verification fails, the user can step through the symbolic execution trace and inspect the symbolic state at each step. Since verification typically takes less than a second, this enables an efficient iterative annotate-and-verify process. Furthermore, it is hoped that by offering proof technology in a form recognizable to programmers, the approach brings interactive program verification to a wider audience. 1