Résumé
Le troisième séminaire de l'année, présenté en anglais, a été consacré à l'outil VeriFast de vérification modulaire et semi-automatique de programmes C et Java à base de logique de séparation.
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.
