By Bart Jacobs, Jan Smans and Frank Piessens,
with contributions by
Jan Tobias Muehlberg,
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.
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):
- 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: 2012-12-13)
- 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.
- 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.
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)]
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
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.
- The Belgian electronic identity card: a verification case study
By Pieter Philippaerts, Frédéric Vogels, Jan Smans, Bart Jacobs, and Frank Piessens.
In Proc. International Workshop on Automated Verification of Critical Systems (AVOCS'11), Newcastle, 12-14 September 2011.
- Sound formal verification of Linux's USB BP keyboard driver
By Willem Penninckx, Jan Tobias Mühlberg, Jan Smans, Bart Jacobs, and Frank Piessens.
In Proc. NASA Formal Methods (NFM 2012), Norfolk, Virginia, USA, 3-5 April 2012.
- Software verification with VeriFast: industrial case studies
By Pieter Philippaerts, Jan Tobias Mühlberg, Willem Penninckx, Jan Smans, Bart Jacobs, and Frank Piessens.
Science of Computer Programming, 2013.
- VeriFast for Java: A Tutorial
By Jan Smans, Bart Jacobs, and Frank Piessens.
In Dave Clarke, Tobias Wrigstad, and James Noble (Eds.), Aliasing in Object-Oriented Programming, LNCS 7850, Springer, 2013.
This work is supported in part by the Flemish Research Fund (FWO-Vlaanderen) and by the EU FP7 project SecureChange.
Last modification: 2013-11-19