VeriFast
By Bart Jacobs, Jan Smans and Frank Piessens,
with contributions by Cedric Cuypers,
Lieven Desmet,
Jan Tobias Muehlberg,
Pieter Philippaerts,
Willem Penninckx,
Thomas Van Eyck,
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.
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.
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):
- The VeriFast program verifier. [PDF]
By Bart Jacobs and Frank Piessens. Technical Report CW-520, Department of Computer Science, Katholieke Universiteit Leuven, Belgium, August 2008.
- The VeriFast Program Verifier: A Tutorial (last update: 2010-11-17)
- Tutorial example file: illegal_access.c. (All tutorial examples are also in the VeriFast distribution.)
- Verification of Imperative Programs: The VeriFast Approach. A Draft Course Text. [PDF]
By Bart Jacobs, Jan Smans, and Frank Piessens. Technical Report CW-578, Department of Computer Science, Katholieke Universiteit Leuven, Belgium. March 2010.
Presents a formalization and soundness proof of a core subset of the VeriFast approach.
- Verifying the Composite Pattern using Separation Logic. [PDF]
By Bart Jacobs, Jan Smans, and Frank Piessens. SAVCBS 2008 Composite pattern challenge track. October 2008.
- Dynamic Owicki-Gries reasoning using ghost fields and fractional permissions. [PDF]
By Bart Jacobs and Frank Piessens. Technical Report CW-549, Department of Computer Science, Katholieke Universiteit Leuven, Belgium. June 2009.
- Verification of data-race-freedom of a Java chat server with VeriFast. [PDF]
By Cedric Cuypers, Bart Jacobs, and Frank Piessens. Technical Report CW-550, Department of Computer Science, Katholieke Universiteit Leuven, Belgium. June 2009.
- Modular full functional specification and verification of lock-free data structures. [PDF] Superseded by CW-590.
By Bart Jacobs and Frank Piessens. Technical Report CW-551, Department of Computer Science, Katholieke Universiteit Leuven, Belgium. June 2009.
- Expressive Modular Fine-Grained Concurrency Specification.
[PDF]
[Coq proof]
By Bart Jacobs and Frank Piessens. Technical Report CW-590, Department of Computer Science, Katholieke Universiteit Leuven, Belgium. July 2010. Revised, August 2010.
Erratum for the July 2010 version.
- VeriFast: Imperative Programs as Proofs. [PDF]
By Bart Jacobs, Jan Smans, and Frank Piessens. Presented at the VS-Tools workshop at VSTTE 2010. August 2010. (No formal proceedings.)
- A Quick Tour of the VeriFast Program Verifier. [PDF]
By Bart Jacobs, Jan Smans, and Frank Piessens. In Proc. APLAS 2010, tool paper track. LNCS 6461, pp. 304-311, November 2010.
- Expressive Modular Fine-Grained Concurrency Specification.
[PDF]
[Slides (PDF)]
[TR]
[Coq proof]
By Bart Jacobs and Frank Piessens. In Proc. POPL 2011. ACM SIGPLAN Notices 46(1), pp. 271-282, January 2011.
- Verification of unloadable modules.
[PDF] [Slides (PDF)]
[TR]
[Coq proof]
By Bart Jacobs, Jan Smans, and Frank Piessens. In Proc. FM 2011.
- The VeriFast Program Verifier: A Tutorial for Java Card Developers [PDF] (Note: for "the VeriFast tutorial", see above.)
- VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java
[PDF]
By Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. Invited paper. In Proc. NASA Formal Methods (NFM) 2011.
Describes: the basic symbolic execution approach in some formal detail; permission accounting (fractions and counting) and precise predicates; lemma function termination.
This work is supported in part by the Flemish Research Fund (FWO-Vlaanderen) and by the EU FP7 project SecureChange.
Last modification: 2011-12-20