Qu’est-ce que la vérification formelle?

Cette séance de cours introduit la vérification formelle comme méthode pour prouver rigoureusement que les systèmes informatiques satisfont à une spécification en définissant des notions mathématiquement rigoureuses et en utilisant des outils automatisés. Une comparaison avec les tests est faite, soulignant les avantages de la vérification formelle par rapport aux méthodes de test traditionnelles. La faisabilité de la démonstration automatisée des théorèmes est discutée, montrant comment les vérificateurs de logiciels modernes peuvent gérer efficacement des théorèmes mathématiques complexes. Le processus de compilation des déclarations d'exactitude du programme en conditions de vérification est expliqué, en soulignant l'importance de transformer les propriétés en formules valides.