| Enseignant | Site/Liens | Cours | TD | TP | ECTS |
|---|---|---|---|---|---|
| Cours : J. Narboux TP : N. Magaud, P. Schreck | Lien externe | 18 | 18 | ||
| Objectifs | |||||
| - Apprentissage des outils de preuve formelle et de certification de logiciels | |||||
| - Utilisation de l'outil Coq pour décrire, prouver et extraire des programmes certifiés | |||||
| Contenu | |||||
| Techniques et systèmes de spécification et de preuve de logiciels. | |||||
| Rôles des mathématiques, de la logique et de la programmation. | |||||
| Définition de types, fonctions, propositions et preuves. | |||||
| Lien entre type et proposition, fonction et preuve. | |||||
| Paramétrage par des données simples, des types ou des propositions. | |||||
| Définitions et preuves par induction. Uitlisation de l’assistant de preuve Coq. | |||||
| Notions de certification et d’extraction de programmes corrects à partir de preuves. | |||||
| Prérequis | |||||
| sémantique et spécifications algébriques (M1S1 I) | |||||
| Références | |||||
| Yves Bertot and Pierre Castéran. Interactive Theorem Proving And Program Development: Coq'art: The Calculus Of Inductive Constructions. Series: Texts in Theoretical Computer Science. An EATCS Series 2004, XXV, 469 p., Hardcover ISBN: 3-540-20854-2 |
|||||
| Contrôle des Connaissances | |||||
| Contrôle continu : coeff. 1/3 | |||||
| Examen écrit : coeff. 2/3 (durée : 2h) | |||||