Software Verification Master 2, 2023–2024

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.

  1. Inductive invariant checking. [Assignment] [Solution]
  2. Numerical abstract domains. [Assignment] [Solution]
  3. Static abstract interpretation. [Assignment] [Solution]
  4. Finer abstract guards. [Assignment] [Solution]
  5. Abstract domain of intervals. [Assignment] [Solution]
  6. 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 to avoid (or at least limit) problems.

  1. Install the opam package via your GNU/Linux distribution's package manager.
  2. Initialize your opam installation with the following command:
    opam init
    eval $(opam env)
    
  3. Create a switch to use version 4.12.1 of the OCaml compilers:
    opam switch create 4.12.1
    eval $(opam env)
    
  4. Install the required opam packages:
    opam install ocamlfind ocamlbuild dune odoc menhir zarith.1.12 z3.4.8.11
    

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

References

Bibliography

Links

OCaml Documentation

Previous Exams