### 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 participants are invited to verify small yet challenging programs using an on-line version of Why3.

### Material

Slides (PDF)Lecture notes (PDF)

Files used during the demos:

`demo_logic.mlw`*Checking a Large Routine*(Turing, 1949)- John McCarthy's 91 function
- Boyer and Moore's MJRTY algorithm
- Same fringe
- Ring buffer
`demo_uf.mlw`- 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

- Historical papers:
- Alan M. Turing. Checking a large routine. 1949.
- C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Communications of the ACM. 1969.

- References from the lecture:
- logic of Why3: CADE 2013, FroCos 2011, VSTTE 2014, Boogie 2011
- WhyML: CAV 2014 (ghost code), hal-01256434 (tracking aliases)
- beyond the lecture: VSTTE 2015 (arithmetic overflows), VSTTE 2016 and IJCAR 2018 (proof by reflection), ARITH 2007 (floating-point programs)

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