Partager cette page :
Discipline(s) : Infomatique et télécommunications

Analyse et conception formelle

Semestre Semestre 1
Type Facultatif
Nature UE
Crédits ECTS 5

Responsables


Contacts

 

Pré-requis

Maitrise de la programmation. Connaissances de base en logique.

Objectifs

L’UE ACF vise à initier les étudiants à l’utilisation de méthodes formelles pour la spécification et le développement de logiciels sûrs. L’accent est mis sur la compréhension des formules logiques et sur leur utilisation pour la spécification de propriétés de programmes. Les programmes considérés seront définis dans un style fonctionnel. L'outil de développement formel utilisé est Isabelle/HOL et le langage d'exportation et d'intégration choisi est Scala. Voir la page de l'UE.

A l’issue de cette UE, l’étudiant doit être capable de programmer une application dans un langage de type fonctionnel et de définir en logique les propriétés attendues de cette application. Il doit, également, être en mesure de formaliser les programmes et les propriétés à l’aide d’un assistant de preuve et de mener à bien leur vérification dans cet outil.

Contenu

Cours :
- Logique propositionnelle, logique du premier ordre et modèles.
- Termes, fonctions, lambda-calcul et types
- Fonctions récursives
- Principes et tactiques de preuve
- Programmation certifiée
- Techniques de vérification de programmes

Travaux dirigés

Travaux pratiques :
- Mise en situation : tentative de programmation correcte d’un algorithme non trivial
- Initiation à la programmation et à la preuve dans un assistant de preuve (Isabelle/HOL)
- Reprise de l’algorithme de mise en situation, reprogrammation et vérification dans l’assistant de preuve
- Initiation à la programmation Scala
- Projet 1 : programmation et vérification d’un analyseur statique
- Projet 2 : programmation et vérification d’un outil de validation de transaction commerciales
 

Contrôles des connaissances

Examen terminal et 2 notes de travaux pratiques sur le Projet 1 et 2.

Mise à jour le 9 novembre 2017