Title: A quick tour of the VeriFast program verifier
Authors: Jacobs, Bart
Smans, Jan
Piessens, Frank #
Issue Date: 28-Nov-2010
Publisher: Springer-Verlag
Host Document: Programming Languages and Systems (APLAS 2010) pages:304-311
Conference: Asian Symposium on Programming Languages and Systems edition:8 location:Shanghai, China date:28 November - 1 December 2010
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 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:
Publication status: published
KU Leuven publication type: IC
Appears in Collections:Informatics Section
# (joint) last author

Files in This Item:
File Description Status SizeFormat
aplas2010-verifast.pdf Accepted 163KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.

© Web of science