Software formal analysis and design

Objectifs pédagogiques

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.

Description de cours

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.

Compétences

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 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)
  • Initiation à la programmation Scala
  • Projet 1 : programmation et vérification d’un outil de comparaison de
    politique de sécurité pour un firewall simplifié
  • Projet 2 : programmation et vérification d’un analyseur statique
  • Projet 3 : programmation et vérification d’un outil de validation de transaction commerciales

Bibliographie

• La page du cours Analyse et conception formelle par Thomas Genet
• A short Isabelle/HOL tutorial for the Functional Programmer by Thomas Genet, 2017
• L’assistant à la preuve Isabelle/HOL, 2022
• Logique pour l’informatique, by Jean-François Raskin
• Programming in Scala (1st edition), by Martin Odersky, Lex Spoon, and Bill Venners, 2008

Biographie de l’enseignant

Thomas Genet is a professor in computer science at ISTIC (Université de Rennes) and a researcher in the Celtique team at IRISA. His research focuses on Verification, Term Rewriting, Tree Automata, Reachability analysis over Term Rewriting Systems, Cryptographic Protocol Verification and Blockchains and smart contract semantics.