1-Fiche descriptive

1) Pré-requis

Aucun

2) Description/Compétences acquises

L'objectif principal de ce cours est l'apprentissage des outilsalgébriques utilisés pour formaliser le développement delogiciels. Ces outils théoriques seront mis enpratique en liaison avec la spécificationet la vérification formelle de programmes.

Notions acquises :

  • Notion de système formel et de règles d'inférence
  • Logique des propositions et des prédicats (Modélisation, Tables de vérité, Déduction naturelle, Principe de résolution, Assistant de preuve Coq)

  • Théorie des ensembles (Termes algébriques, Preuve par induction, Application avec Coq)

  • Logique de Hoare, Preuve de terminaison, Spécification et preuve de correction, Application à Why

  • Théorie des langages (Automate fini, Automate à pile, Grammaire, Expression régulière, Transformation automates/expressions régulières), Application avec lex et yacc

  • Point fixe d'une fonctionnelle

3) Liste des matières

Non renseignée

3 - Responsables

  • Gergaud Joseph
  • Massoutie-camus Christiane