A Quick Tour of the VeriFast Program Verifier

Speaker Jan Tobias Muehlberg, Department of Computer Science, K.U.Leuven, Belgium

Location: 701, Claremont Tower
Date/Time: 24th May 2011, 14:00 - 15:00

In this talk I will give a practical introduction to the VeriFast program
verifier. I will focus on ongoing research in which our verifier is applied
to low-level systems code such as operating system components and network
management software.

VeriFast is a sound and modular verification tool for C and Java. It takes
as input a number of source files annotated with method contracts written
in separation logic, inductive data type and fixpoint definitions, lemma
functions and proof steps. The verifier checks that (1) the program does
not perform illegal operations such as dividing by zero or illegal memory
accesses 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
verification 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:
http://www.cs.kuleuven.be/~bartj/verifast

Published: 9th May 2011