A Quick Tour of the VeriFast Program Verifier

Abstract. This paper describes the main features of VeriFast, a sound and modular program verifier for C and Java. VeriFast takes as input a number of source files annotated with method contracts written in sep-aration logic, inductive data type and fixpoint definitions, lemma func-tions and proof steps. The verifier checks that (1) the program does not perform illegal operations such as dividing by zero or illegal memory ac-cesses and (2) that the assumptions described in method contracts hold in each execution. Although VeriFast supports specifying and verifying deep data structure properties, it provides an interactive verification experience as verifica-tion times are consistently low and errors can be diagnosed using its symbolic debugger. VeriFast and a large number of example programs are available online at