Vérification des 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

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

Contrôle des connaissances

SESSION 1

épreuve terminale de 3h, coefficient 2/3,

Contrôle continu, coefficient 1/3

SESSION 2

épreuve écrite (3h) ou orale selon l’effectif, coeff 2/3,

report de la note finale de contrôle continu, coeff 1/3 ;

note finale session 2 : max(note examen 2, 2/3* note examen 2 + 1/3 note contrôle continu)

Lectures recommandées

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

Responsable de l'unité d'enseignement

Jerome Leroux

Enseignants

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