UE ACF

Analyse et Conception Formelles

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.

Compétences acquises

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.

Responsable

Thomas Genet (thomas [dot] genetatirisa [dot] fr)