Vérification de Logiciels

Informations

Langue d'enseignement : Anglais
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 :
L'enseignement présente les structures de données partagées comme les BDD (Binary Decision Diagrams), l'analyse de programmes par interprétation abstraite, les algorithmes de type CEGAR, et les techniques de résolution du problème SAT avec interpolation. Les thèmes suivants sont abordés : vérification symbolique de modèles finis, analyse statique, et vérification par abstraction.

---

This course presents shared data structures, like BDD (Binary Decision Diagrams), program analysis by abstract interpretation, CEGAR algorithms, and SAT solving techniques based on interpolation. The following topics are presented: symbolic verification of finite models, static analysis, and verification through abstraction.

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

  • 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)

Organisation pédagogique

- Non défini -

Contrôle des connaissances

Épreuve terminale de 3h, coefficient 2/3

Contrôle continu, coefficient 1/3

Pas de deuxième session.

Lectures recommandées

- Non défini -

Responsable de l'unité d'enseignement

Jerome Leroux

Enseignants

- Non défini -