CS5008E - Formal methods based V&V 2

Objectifs

Objectif général :

Expertise in formal verification methods, with a focus on deductive methods and abstract interpretation

Objectifs détaillés :

The student will:

be able to explain the soundness/unsoundness, completeness/incompleteness and termination/non termination properties of each method.
be able to explain the reasoning behind deductive methods
be able to explain the key elements of abstract interpretation
be able to implement a non relational abstract domain and apply the analysis