VeriFast is a verification tool for single- and multi-threaded 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. VeriFast comes with an IDE that enables interactive annotation insertion and symbolic debugging.

So far, we have used VeriFast to experiment with novel approaches for modular specification and verification of functional correctness of fine-grained concurrent algorithms [POPL 2011], memory-safety of programs that dynamically load and unload modules [FM 2011], the interactive behavior of programs that use APIs like stdio.h or java.io [ESOP 2015], termination of programs involving dynamically bound method calls [ECOOP 2015], and deadlock-freedom of programs where threads wait for other threads in the presence of exceptions [FTfJP 2015]. Furthermore, we have used VeriFast to verify crash-freedom of Java Card software for the Belgian eID card, a Linux device driver, a C program routing packets in a home gateway, and functional correctness of the complex Multiple-Compare-and-Swap lock-free concurrent algorithm, and to participate in verification competitions, winning at VerifyThis 2012 and 2016.

VeriFast is available for download at https://people.cs.kuleuven.be/~bart.jacobs/verifast/.

Assistant professor at the iMinds-DistriNet research group at the Department of Computer Science, KU Leuven - University of Leuven, Belgium