L’objectif de cette UE sera d’aborder le thème de la vérification de programmes critiques, à l’aide de méthodes formelles comme le model-checking. Le cours présentera les outils permettant de modéliser de façon formelle le logiciel à vérifier, ainsi que les propriétés étudiées. Les algorithmes de vérification associés seront ensuite présentés, et illustrés au travers d’outils logiciels. Une approche qui pourra par exemple être présentée est la vérification de propriétés linéaires LTL via les automates de mots finis et infinis. Cette approche sera illustrée à l’aide de l’outil SPIN.