VeriFast is a leading tool for modular formal verification of C and Java programs. The user inserts functional correctness specifications for each function/method and proof hints into the source code as specially marked comments in a separation logic notation and then presses Play. The tool then uses these to perform symbolic execution of each function/method in isolation and, typically in a matter of seconds, either reports “0 errors found”, meaning that all of the program’s executions are crash-free and comply with the stated specifications, or shows a failing symbolic execution trace in a debugger-like GUI. In this talk, we give a VeriFast tutorial, covering the basics as well as how to deal with complex pointer structures and concurrency. We also discuss the problem of modular verification of I/O in separation logic, and showcase the solution we have developed in recent work.

Bart Jacobs is an associate professor at the Department of Computer Science at KU Leuven in Belgium. After contributing to Spec# as an intern with Wolfram Schulte and Rustan Leino at Microsoft Research Redmond, he has been developing VeriFast since 2008. Research results (published at ECOOP and elsewhere) include approaches for modular verification of safety and liveness of pointer-manipulating programs in the presence of unchecked exceptions, fine-grained concurrency, condition variables, and I/O.

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