On May 2021, Bart Jacobs presented the operation mode of VeriFast at Vortex, as well as shared an overview of the verification tasks, that with this tool, he and his team have performed so far. He also compared the strengths and weaknesses of VeriFast with other available technologies.
Bart Jacobs explained that VeriFast takes as input the source code for a C or Java module, annotated with function/method preconditions and postconditions expressed in separation logic, as well predicates expressing the shapes and contents of data structures and recursive lemmas serving as inductive proofs. As a result, and in a matter of seconds, this technology returns either a “0 errors found” message or a symbolic execution trace leading to a verification failure. In the former case, assuming the other modules of the program satisfy the provided specifications, and barring bugs in VeriFast, can be concluded that no execution of the program accesses unallocated memory, performs data races, or violates the specified properties.
About Bart Jacobs:
Since 2010, Bart Jacobs is an associate professor at the Department of Computer Science at KU Leuven, Belgium’s largest university. He did his PhD at KU Leuven, under the supervision of Frank Piessens, during which he interned extensively at the Spec Team of Wolfram Schulte and Rustan Leino at Microsoft Research, in Redmond. He has published about Hoare logics for fine-grained concurrency, exception handling, deadlock-freedom, I/O, termination, and general liveness properties and is the main developer of VeriFast.