Programmes de vérification avec l'inox: Partie 2

Cette séance de cours couvre l'utilisation d'Inox pour la vérification des programmes, en mettant l'accent sur la vérification des programmes et en assurant l'exactitude. L'instructeur démontre le processus d'utilisation d'Inox pour vérifier les programmes, y compris la définition des spécifications, la garantie des conditions post-conditions et la vérification de la résiliation. La séance de cours comprend également des exemples de fonctions de vérification, telles que non EmptyListSize et zip, à l'aide de solveurs Inox et SMT. On souligne l'importance de définir les conditions et les mesures post-récursives pour les fonctions récursives, ainsi que l'importance d'assurer l'exactitude des conditions de vérification. La séance de cours se termine par une discussion sur le pouvoir de l'inox dans la vérification précise des programmes et la contribution de divers chercheurs et collaborateurs au projet.