Une introduction à CompCert et Coq

Dans le cadre du cours ACSS en Ensimag 2A, voilà une présentation de CompCert (un compilateur C certifié) et Coq (un assistant de preuves ayant permis de certifier CompCert):

  1. Télécharger les diapos (ou leur version 4 par pages) et suivre la vidéo pour avoir le commentaire audio sur les diapos.
  2. Compléter en parcourant le mini-tutoriel (optionnel) en ligne: comment définir un mini-calcul de WP en Coq.
  3. et/ou la démo (optionnelle) en vidéo de CompCert.
N'hésitez pas à m'écrire à Sylvain.Boulme@imag.fr pour toute question, commentaire ou suggestion.