Introduction à la vérification formelle

Cette séance de cours présente les principes et la pratique de la vérification formelle, en mettant l'accent sur la construction de logiciels vérifiés à l'aide d'outils et la compréhension des principes sous-jacents. Le cours met l'accent sur la preuve rigoureuse que les systèmes informatiques satisfont aux spécifications, en contrastant la vérification formelle avec les tests. Il couvre des sujets tels que la démonstration automatique des théorèmes, la compilation de programmes en formules et limportance des modèles mathématiques pour assurer lexactitude du système.