Ingénierie de la preuve

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)

Notes

 
m1ilc/preuves.txt · Dernière modification: 2011/04/09 08:26 par suitable
 
Sauf mention contraire, le contenu de ce wiki est placé sous la licence suivante :CC Attribution-Noncommercial-Share Alike 3.0 Unported
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki