Software Verification — Master 2, 2024–2025

Slides

Exercises

Lab Sessions

The course includes lab sessions devoted to the step-by-step implementation of a simple program analyzer. Developments are realized in OCaml. See below for the required OCaml environment.

Inductive invariant checking. [Assignment] [Solution]
Numerical abstract domains. [Assignment] [Solution]
Static abstract interpretation. [Assignment] [Solution]
Finer abstract guards. [Assignment] [Solution]
Abstract domain of intervals. [Assignment] [Solution]
Widening and narrowing. [Assignment] [Solution]

OCaml Environment

Lab Computers

If you use one of the fixed computers running GNU/Linux available in the lab rooms then you should use the global opam installation. To do so, simply execute the following commands:

export OPAMROOT=/opt/local/opam
eval $(opam env)

Personal Computers

If you use a personal computer running GNU/Linux, then you should set up your OCaml environment as follows. This reproduces the global opam installation of the lab computers.

Install the opam package via your GNU/Linux distribution's package manager.
Initialize your opam installation with the following command:
```
opam init
eval $(opam env)
```
Create a switch to use version 5.1.0 of the OCaml compilers:
```
opam switch create 5.1.0
eval $(opam env --switch=5.1.0)
```

Install the required opam packages:

opam install ocamlfind ocamlbuild dune odoc menhir zarith.1.13 z3.4.12.2-1

Do not forget to execute the command eval $(opam env --switch=5.1.0) whenever you want to use your local opam installation.

References

Bibliography

A. Miné. Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation. In Foundations and Trends in Programming Languages, 4(3–4):120–372, 2017. [hal]
F. Nielson, H.R. Nielson and C. Hankin. Principles of Program Analysis. Springer, 1999. [www]
U. Khedker, A. Sanyal and B. Sathe. Data Flow Analysis: Theory and Practice. CRC Press, 2009. [www]
P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. In Journal of Logic Programming, 13(2--3):103--179, 1992. [www]
P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In Proc. PLILP'92, LNCS 631. Springer, 1992. [www]

OCaml Documentation

Learn Ocaml.
OCaml Tutorials: A Tour of OCaml, Modules, and more.
OCaml Manual.