Abstract

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.).

Material

Slides (PDF)

Lecture notes (PDF)

Files used during the demos:

Exercises

To perform the exercises, you have to first install Why3 and one or several theorem provers. Relevant instructions are given on
Why3's web site. Why3 is launched with the following command: why3ide file.mlw

For each exercise, a file is provided and must be completed. The various questions are given at the beginning of the file.

  1. Dijkstra's Dutch national flag problem: exo_flag.mlw (solution)
  2. Ring buffer: exo_buffer.mlw (solution)
  3. Inorder traversal of a tree: exo_fill.mlw (solution)