Software verification

The main aim of this course is to introduce classical verification techniques and implement them in a (simple) program verifier. The tool produced during the semester is capable of detecting assertion violations on programs in a sub-language of C (only integers and no pointers) without the user having to provide any information other than the program.

Part 1:

General framework of the checker (including the language checked and its semantics), aimed at familiarizing you with the language used (Ocaml) and the SMT-solver used (Z3), and presentation of the Bounded Model Checking technique through two algorithms to achieve it.

Part 2:

Introduction to abstract interpretation, which involves looking at abstractions of the set of executions of a program in a simpler, well-ordered mathematical domain. In this section, several simple abstract domains are implemented.

Part 3:

Presentation of the counter-example guided abstraction refinement (CEGAR) technique and some basics on Petri nets.