Comment vérifier formellement des programmes avec Coq ?

Comment vérifier formellement des programmes avec Coq ?

La deuxième session de cours de l’école d’été mathinfoly 2019 est conduite par Dr. Catalin Hricu, chercheur à l’INRIA Paris.

Son cours se concentre sur l’assistant de vérification de programmes appelé COQ et l’apprentissage de la programmation fonctionnelle pour implémenter l’assistant et vérifier des théorèmes de logique.

Un cours certes exigeant pour les étudiants mais qui a pu se concrétiser grâce aux multiples TDs accompagnés par la Reserach Squad de Catalin : Jérémy, Exequiel, Roberto et Florian.

Vous retrouverez l’ensemble du cours et des exercices sur le lien suivant : https://prosecco.gforge.inria.fr/personal/hritcu/teaching/lyon2019/.

Suivez-nous :

Les commentaires sont clos.
Facebook
Facebook
RSS