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

- Non défini -

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

- Non défini -

Responsable de l'unité d'enseignement

Anca Muscholl

Enseignants

- Non défini -