Cours Ingénierie de la preuve (M1S2 - Informatique) / Certification du Logiciel (M2S3 - ISI)

Documents utiles pour les cours, TDs et TPs

• la fonction puissance et quelques preuves
• modeles2.v : les modeles de voitures
• Scripts de preuve du cours 1
• Scripts de preuve du cours 2
• Scripts de preuve du cours 2 (suite)

Anciens sujets d'examens

• contrôle continu de mars 2009
• sujet de projet de mars 2009 (proposition de correction)
• sujet d'examen de septembre 2008
• contrôle continu de mars 2008
• sujet d'examen de septembre 2007
• contrôle continu de mars 2007 (proposition de correction)
• sujet d'examen de septembre 2006
• contrôle continu de mai 2006 (proposition de correction)

Bibliographie et liens vers d'autres cours

• Yves Bertot & Pierre Castéran. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Springer. 2004
• Coq homepage (Manuel de référence)
• Exercices du Coq'Art
• Exercices par Laurent Théry
• Formal Proof (numéro spécial de Notices of the American Mathematical Society)
• Théorie des types et mathématiques certifiées (dans la Gazette des Mathématiciens #142, Octobre 2014)