VeriFast

By Bart Jacobs, Jan Smans and Frank Piessens, with contributions by Pieter Agten, Cedric Cuypers, Lieven Desmet, Jan Tobias Muehlberg, Willem Penninckx, Pieter Philippaerts, Thomas Van Eyck, Gijs Vanspauwen, and Frédéric Vogels

VeriFast is a verifier for single-threaded and multithreaded C and Java programs annotated with preconditions and postconditions written in separation logic. To enable rich specifications, the programmer may define inductive datatypes, primitive recursive pure functions over these datatypes, and abstract separation logic predicates. To enable verification of these rich specifications, the programmer may write lemma functions, i.e., functions that serve only as proofs that their precondition implies their postcondition. The verifier checks that lemma functions terminate and do not have side-effects. Since neither VeriFast itself nor the underlying SMT solver need to do any significant search, verification time is predictable and low.

Download VeriFast below, or try a bare-bones version online at rise4fun!

Starting with version 7.0, VeriFast has support for verifying full functional partial correctness of lock-free data structures and their clients. See the TR below and the queue example.

New in release 7.2: a proof of Harris et al.'s lock-free MCAS algorithm. See the examples.

New in release 7.3: a proof of a fine-grained concurrent set of integers implemented as a linked list with hand-over-hand locking. See the examples.

New in release 9.0: support for verifying unloadable modules and the programs that use them, such as operating system kernels that load and unload device drivers. See the MockKernel example.

Bart and Jan, using VeriFast, won the VerifyThis verification competition at Formal Methods 2012.

Subscribe to the VeriFast RSS feed to be informed of new releases and documentation updates.

VeriFast uses the Z3 SMT solver produced by Leonardo de Moura and Nikolaj Bjørner at Microsoft Research. Z3 is included in the distribution. The Z3 license applies.

The distribution includes the verifier both as a command-line tool (verifast.exe), and in the form of an IDE (vfide.exe). In the IDE, if an execution path fails, you can browse through the execution path and inspect the memory representation and the set of assumptions at each point.

Example programs (also included in the distribution)

Documentation (under construction):

This work is supported in part by the Flemish Research Fund (FWO-Vlaanderen) and by the EU FP7 project SecureChange.

Last modification: 2013-04-12