Deductive Program Verification with Why3

Jean-Christophe Filliâtre, LRI, CNRS & University Paris-Sud, Orsay, France.

This lecture is an introduction to deductive program verification and to the tool Why3. This tool provides an imperative programming language (with polymorphism, algebraic data types, pattern matching, exceptions, references, arrays, etc.), a specification language that is an extension of first-order logic, and a technology to verify programs using interactive and automated theorem provers (Coq, Alt-Ergo, Z3, CVC3, etc.). Through many examples, this lecture introduces elementary concepts of program verification (pre- and postconditions, loop invariants, variants, ghost code, etc.) as well as techniques (specification, termination proofs, modeling of data structures, etc.).