Abstract

This lecture introduces elementary concepts and techniques related to deductive program verification, such as loop invariants, function contracts, termination proofs, ghost code, modeling of data structures, weakest preconditions, etc. A particular focus is made on the use of automated theorem provers in the verification process and the tension that may exist between an elegant specification and a fully automated proof. The lecture includes many examples using
the Why3 tool and lab sessions will invite participants to formally verify small yet challenging programs using Why3.

Material

Slides (PDF)

Lecture notes (PDF)

Files used during the demos:

Lab

The labs use this on-line version of Why3. You have to select an exercise in the top menu and then to complete the input file. The questions are given at the beginning of the file. If needed, you can browse the Why3 standard library.

If you choose instead to install Why3 on your laptop, the input files for the exercises are contained in this lab.zip archive. The Why3 GUI is launched with the following command: why3 ide file.mlw

All input files and solutions:

  1. Euclidean division: ex1_eucl_div.mlw (solution)
  2. Factorial: ex2_fact.mlw (solution)
  3. Ancient Egyptian multiplication: ex3_multiplication.mlw (solution)
  4. Two way sort: ex4_two_way.mlw (solution)
  5. Dijkstra's Dutch national flag: ex5_flag.mlw (solution)
  6. Ring buffer: ex6_buffer.mlw (solution)
  7. Inorder traversal of a tree: ex7_fill.mlw (solution)

Further Reading

Other Deductive Verification Tools

Acknowledgments
I'm grateful to Martin Clochard, Kim Nguyen, and Mário Pereira for their help in the preparation of this lecture.

 


INRIA Saclay - Île-de-France              Université Paris-sud              CNRS              LRI