AccueilLicence généraleInformatiqueEnseignementsIntroduction à la vérification

Licence InformatiqueUE Introduction à la vérification

Contenu

L’objectif de cette UE sera d’aborder le thème de la vérification de programmes critiques, à l’aide de méthodes formelles comme le model-checking. Le cours présentera les outils permettant de modéliser de façon formelle le logiciel à vérifier, ainsi que les propriétés étudiées. Les algorithmes de vérification associés seront ensuite présentés, et illustrés au travers d’outils logiciels. Une approche qui pourra par exemple être présentée est la vérification de propriétés linéaires LTL via les automates de mots finis et infinis. Cette approche sera illustrée à l’aide de l’outil SPIN.

Compétences visées

  • Utiliser les concepts fondamentaux de l'informatique (langages formels, logique, et graphes) pour la programmation et la modélisation.
  • Connaître des pratiques, outils et techniques visant à assurer la sécurité des systèmes informatiques pendant leur développement et leur utilisation.
  • Se servir aisément des bases de la logique pour valider ou réfuter un raisonnement.
  • Faire preuve d'esprit critique vis-à-vis d'une solution technique pour en vérifier son efficacité, sa fiabilité et sa robustesse dans son contexte d'utilisation.

Langue utilisée

Langue principale utilisée par cet enseignement : Français.

Pré-requis recommandés

  • Logique
  • Langages formels

Volume des enseignements

  • Cours magistraux : 9 heures
  • Travaux dirigés : 10 heures
  • Travaux pratiques : 10 heures

Les formations qui utilisent cet enseignement