Semestre 8 – Option – Preuves et démonstration automatisée

Objectifs

Cette UE présente les méthodes et techniques de base de la compilation des langages principalement impératifs ainsi que la certification via les machines abstraites.

Prérequis

Voir la description des prérequis du M1.

Contenu pédagogique de l’UE

  • Systèmes formels (calculs de prédicats).
  • Procédures de preuves :
    • tableaux, résolution
    • connexions
  • Traitement de l’égalité.
  • Implantation des procédures.