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.
New in release 14.12: support for specifying and verifying I/O properties (see examples/io), as well as termination and liveness properties (see examples/termination). See the relevant publications below.
Bart and Jan, using VeriFast, won the VerifyThis verification competition at Formal Methods 2012.
VSComp 2014: log-based concurrent set: Post-competition solution in VeriFast.
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.
(* These releases do not include or support the Z3 SMT solver; they use the built-in Redux SMT solver that we developed in-house. Some of the test cases from the test suite, which verify with Z3 but not with Redux, are disabled in these releases.)
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: 2014-10-08)
- 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 82(1), pp. 77-97, March 2014.
- 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.
- Sound symbolic linking in the presence of preprocessing
By Gijs Vanspauwen and Bart Jacobs.
In Proc. 11th International Conference on Software Engineering and Formal Methods (SEFM 2013), LNCS 8137, Springer, 2013.
- Solving the VerifyThis 2012 challenges with VeriFast
By Bart Jacobs, Jan Smans, and Frank Piessens.
In International Journal on Software Tools for Technology Transfer, 2014.
- Verifying TSO programs
By Bart Jacobs.
Technical report CW660, Department of Computer Science, KU Leuven, May 2014.
- Shared boxes: rely-guarantee reasoning in VeriFast
By Jan Smans, Dries Vanoverberghe, Dominique Devriese, Bart Jacobs, and Frank Piessens.
Technical report CW662, Department of Computer Science, KU Leuven, May 2014.
- Sound, modular and compositional verification of the input/output behavior of programs
By Willem Penninckx, Bart Jacobs, and Frank Piessens.
In Proc. ESOP 2015.
- Modular termination verification
By Bart Jacobs, Dragan Bosnacki, and Ruurd Kuiper.
At ECOOP 2015.
- Provably live exception handling
By Bart Jacobs.
At FTfJP 2015.
- Featherweight VeriFast
[Slides, handouts, Coq proof]
By Frédéric Vogels, Bart Jacobs, and Frank Piessens.
In Logical Methods in Computer Science 11(3:19), 2015.
- Verifying protocol implementations by augmenting existing cryptographic libraries with specifications
By Gijs Vanspauwen and Bart Jacobs.
At SEFM 2015.
Third-party research that uses VeriFast:
- Luyi Xing, Xiaorui Pan, Rui Wang, Kan Yuan, and Xiaofeng Wang.
Upgrading Your Android, Elevating My Malware: Privilege Escalation Through Mobile OS Updating.
In Proc. 35th IEEE Symposium on Security and Privacy (IEEE Oakland), 2014.
Third-party resources on VeriFast:
This work is supported in part by the Flemish Research Fund (FWO-Vlaanderen), by the EU FP7 project SecureChange, by Microsoft Research Cambridge as part of the Verified Software Initiative, by the EU FP7 projects ADVENT and STANCE, and by Research Fund KU Leuven.
Last modification: 2016-01-28