AbstractThis 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.
Lecture notes (PDF)
Files used during the demos:
- Checking a Large Routine (Turing, 1949)
- John McCarthy's 91 function
- Boyer and Moore's MJRTY algorithm
- Same fringe
- Ring buffer
- Hash tables
- Binary search
LabThe 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:
- Euclidean division: ex1_eucl_div.mlw (solution)
- Factorial: ex2_fact.mlw (solution)
- Ancient Egyptian multiplication: ex3_multiplication.mlw (solution)
- Two way sort: ex4_two_way.mlw (solution)
- Dijkstra's Dutch national flag: ex5_flag.mlw (solution)
- Ring buffer: ex6_buffer.mlw (solution)
- Inorder traversal of a tree: ex7_fill.mlw (solution)
- Alan M. Turing. Checking a large routine. 1949.
- C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Communications of the ACM. 1969.
Other Deductive Verification Tools
AcknowledgmentsI'm grateful to Martin Clochard, Kim Nguyen, and Mário Pereira for their help in the preparation of this lecture.