Software Verification Master 2, 2020–2021

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.

  1. Inductive invariant checking. [Assignment] [Solution]
  2. Numerical abstract domains. [Assignment] [Solution]
  3. Static abstract interpretation. [Assignment] [Solution]
  4. Abstract domain of intervals. [Assignment] [Solution]
  5. Widening and narrowing. [Assignment] [Solution]

References

Bibliography

Links

OCaml Documentation

Previous Exams