Jean-Christophe Filliâtre’s abstract

This lecture is an introduction to deductive verification. In this approach, the correctness of a program is reduced to a set of mathematical formulas, which are then discharged using automated and/or interactive theorem provers. The lecture will illustrate the main ideas and techniques behind this approach, with a focus on ghostcode.