===== Ingénierie de la preuve =====


^ Enseignant ^ Site/Liens ^ Cours ^ TD ^ TP ^ ECTS ^
| Cours : J. Narboux\\ TP : N. Magaud, P. Schreck | [[http://dpt-info.u-strasbg.fr/~narboux/Enseignement/IngenieriePreuve/2009-2010/index.html|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) ||||||

==== Notes ====
  * [[preuves_1| 29/01/2010]] : introduction, peu de notes car difficile avec diapos passés rapidement.
  * [[preuves_2| ]] : 
  * [[preuves_3| ]]  
  * [[preuves_4| ]]  
  * [[preuves_defs| ]] : un extrait des définitions de types rencontrés en TP (et cours?)
  * [[preuves_tp3| ]] : définition et preuves de propriétés de nombre complexes entiers