École de recherche d'hiver "vérification et certification du logiciel", ENS Lyon, janvier 2012

Sémantiques formelles sur machine

Application à la compilation formellement vérifiée

Support de cours:

• Les transparents: pour présenter et pour imprimer (6 par page).
• Développement Coq sur le langage IMP, commenté, pour être vu en ligne:
  • IMP: syntaxe et sémantiques d'IMP.
  • IMPcompiler: compilation d'IMP vers une machine virtuelle, et sa preuve de correction.
  • Sequences: bibliothèque sur les séquences de transition et leurs propriétés.
• Développement Coq sur le langage IMP, distribution source: IMP.zip.
• CompCert: sources Coq commentées