Introduction à la vérification

Informations

Langue d'enseignement : Français
Crédits ECTS: 6

Programme

  • Heures d'enseignement dispensées à l'étudiant : 48 heures
  • Temps de travail personnel : 102 heures

Objectifs et compétences

Objectifs :
Le cours introduit des techniques de vérification automatique de systèmes : model-checking pour les systèmes finis (systèmes de transitions, logiques temporelles, vérification) et (in-)décidabilité pour les systèmes infinis (automates communicants, automates temporisés, réseaux de Petri,...).

Compétences :
  • Comprendre et mettre en oeuvre l'intérêt et les principes de la démarche de recherche fondamentale et/ou appliquée
  • Construire et développer une argumentation.

  • Maîtriser les bases de la logique et organiser un raisonnement mathématique.
  • Construire et rédiger une démonstration mathématique synthétique et rigoureuse.
  • Être capable de traduire un problème simple en langage mathématique.
  • Évaluer et améliorer la sécurité d'un système d'information
  • Connaître les principaux paradigmes de programmation et sélectionner un langage adapté à une situation donnée
  • Analyser un document scientifique ou technique (y compris du code), en français ou en anglais, en vue de son utilisation dans un contexte informatique
  • Concevoir des algorithmes avancés dans son domaine de spécialisation, et savoir les programmer
  • Utiliser les bibliothèques et outils logiciels usuels de son domaine de spécialisation
  • Comprendre et traduire sous forme algorithmique la spécification mathématique d'une méthode de son domaine de spécialisation
  • Implémenter et/ou comparer les méthodes de l'état de l'art dans son domaine de spécialisation
  • Comprendre une preuve de correction d'algorithme (e.g., variants/invariants, induction, convergence)
  • Ecrire une preuve de correction d'algorithme

Organisation pédagogique

le mode de fonctionnement de l'UE est présenté au début des enseignements

Contrôle des connaissances

Contrôle continu et examen final.

Session 1:

Contrôle continu, coefficient 0.5

Examen final (3h), coefficient 0.5

Session 2:

Contrôle continu: report session 1, coefficient 0.5

Examen écrit (3h) ou oral selon l'effectif, coefficient 0.5

Note finale session 2: max(NoteEx2, 0.5 * NoteEx2 + 0.5 * NoteCC)

Lectures recommandées

l'ensemble des références bibliographiques est communiqué au début des enseignements

Responsable de l'unité d'enseignement

Anca Muscholl

Enseignants

la composition de l'ensemble de l'équipe pédagogique est communiquée au début des enseignements