Software model checking

Enseignants : Sylvain Conchon, Sébastien Bardin

Cours :

Ce cours est une introduction à la technique du model checking qui permet de vérifier automatiquement des propriétés de sûreté et de vivacité des sytèmes. Les outils de model checking sont très utilisés dans le monde industriel, en particulier dans la phase amont du développement de ces systèmes. Le cours présentera à la fois les langages de modélisation et les algorithmes sous-jacents pour vérifier des propriétés de sûreté et vivacité.

TD :

Prérequis :