Abstract
The third seminar of the year, presented in English, was devoted to the VeriFast tool for semi-automated modular verification of C and Java programs, based on separation logic.
Bart Jacobs presented the VeriFast tool for semi-automated modular verification of single-threaded and multithreaded C and Java programs, based on separation logic. The tool takes as input C or Java source code files annotated with special comments containing function/method preconditions and postconditions, loop invariants, data structure definitions in the form of recursive separation logic predicates, mathematical definitions, and proof hints, and usually after a matter of seconds returns either "0 errors found" or a failing symbolic execution trace. Barring bugs in the tool, "0 errors found" means no execution of the program exhibits undefined behavior (such as accesses of unallocated memory or data races) or violates the specified assertions. Bart Jacobs gave an overview of results we obtained so far, and of ongoing work. Most of the talk was a live demonstration.
