The Why and How of Deductive Program Verification

This lecture introduces fundamental concepts and techniques related to deductive program verification, such as function contracts, loop invariants, 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 on the building of a standard library for verification. The lecture includes many examples using the Why3 tool and a lot of small exercises in program verification are provided.

Lecture Slides

• Lecture 1 (Wednesday)
  • kadane.mlw (download)
• Lecture 2 (Thursday)
• Lecture 3 (Friday)
• Lecture 4 (Saturday)
  • alpha_beta.mlw (download)
  • want to play Othello?

Exercises

• maximum subarray problem: ex1_kadane.mlw | view | solution
• peasant multiplication: ex2_3_peasant.mlw | view | solution
• McCarthy's 91 function: ex4_f91.mlw | view | solution
• Fibonacci numbers: ex5_fib.mlw | view | solution

Installing/Using Why3

• Run Why3 in your browser
  • nothing to install
  • but a limited prover back-end

• Install Why3 on your machine

  We strongly suggest using Why3find. Here are installation instructions:

  1. install opam (typically using your system's package manager)
  2. then run the following commands:

         opam init
         opam install why3find alt-ergo
     

  3. if you wish, install a few other SMT solvers, e.g. Z3 and CVC5
  4. configure why3find:

         why3find config --detect
     

     (It detects provers available from your PATH, so be sure z3 and cvc5 binaries can be found.)
  5. you can now run why3find from the command line:

         why3find prove file.mlw
     

  6. if you intend to use VS Code, install the VS Code extension why3-platform

Resources

• Why3
• Why3find
• Why3's gallery of verified programs

• Papers related to the design and implementation of Why3:
  • One Logic To Use Them All (JCF, CADE 2013)

    describes the logic of Why3

  • The Spirit of Ghost Code (JCF, Léon Gondelman, Andrei Paskevich. Formal Methods in System Design, 2016)

    the design of ghost code in Why3

  • When Separation Arithmetic is Enough (JCF, Andrei Paskevich, Olivier Danvy. iFM 2025)

    verification of pointer programs with Why3

  • Abstraction and Genericity in Why3 (JCF, Andrei Paskevich. ISoLA 2021)

    building modular proofs with Why3

  • Avoiding exponential explosion: generating compact verification conditions (Cormac Flanagan, James B. Saxe. POPL 2001)

    how to improve over the traditional way of computing weakest preconditions (this is implemented in Why3)

• Case studies:
  • WhyMP, a Formally Verified Arbitrary-Precision Integer Library (Guillaume Melquiond, Raphaël Rieu-Helft. ISAAC 2020)

    a rather large case study, with a nontrivial subset of GMP's algorithms verified with Why3

  • Design of a Correct-by-Construction Checker for Constraints on Railway-Oriented Databases (Benoît Boyer, Noé Canva, Matteo Manighetti, Claude Marché. Research Report, 2025)

    another case study, with the verification of a checker for a railway information system

• Papers and books not related to Why3:
  • Checking a large routine (Alan M. Turing, 1949) (see also An Early Program Proof by Alan Turing by Morris and Jones, 1984)
  • Assigning Meanings to Programs (Robert W. Floyd, 1967)
  • An Axiomatic Basis for Computer Programming (C. A. R. Hoare, 1969)
  • Program Proofs (Rustan Leino, MIT Press, 2023)
  • Division and Modulus for Computer Scientists (Daan Leijen, 2001)
  • An analysis of alpha-beta pruning (Donald E. Knuth, Ronald W. Moore, 1975)

• Programming Pearls. Jon Bentley. Addison-Wesley Professional, 1999.
• The Practice of Programming. Brian W. Kernighan, Rob Pike. Addison-Wesley Professional Computing Series, 1999

Acknowledgments