Teaching

Decision Procedures for the Verification of Programs, Master Recherche Informatique, Parcours Ingénierie des Logiciels, Orientation Méthodes Formelles pour des Logiciels Sûrs, Université de Lorraine, 2020/21. Taught initially with Silvio Ranise, then with Pascal Fontaine, and now with Sophie Tourret.

1. Introduction
2. Decision Procedures for the theory of Equality
3. Linear Arithmetic
4. Combining Decision Procedures
5. Building Decision Procedures for Data Structures
6. Boolean Solving
7. Integrating Decision Procedures with Boolean Solving
8. Applications: the veriT SMT solver