Vérification des programmes avec l'inox

Cette séance de cours couvre l'utilisation de Stainless, un outil de vérification des programmes, avec un accent sur les propriétés de correction fonctionnelle, des assistants d'épreuve comme Coq et Isabelle, et des vérifications dynamiques. Il traite également de l'automatisation des preuves, de la vérification des logiciels de systèmes et de la vérification de divers systèmes tels que les systèmes de fichiers, les systèmes distribués, les contrats de blockchain et les structures de données. La séance de cours se penche sur l'utilisation de Scala et Inox SMT solveur pour la vérification, l'automatisation des tâches de raisonnement, et la génération de contre-exemples pour aider à la vérification.