### 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:

`demo_logic.why`*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

### 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:

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

### Further Reading

- 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

##### Acknowledgments

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