Sémantique, typage et analyse de programme

Code UE : SMB210

  • Cours
  • 6 crédits

Responsable national

Olivier PONS

Responsable opérationnel

Objectifs pédagogiques

Produire des applications embarquées de confiance en utilisant des analyses de code

Contenu

Il est reconnu que la conception d'applications à haut degré de fiabilité et de sécurité nécessite l'apport des méthodes formelles. Ce cours vise à donner une base théorique et formelle solide sur les aspects nécessaires à la vérification des systèmes embarqués en utilisant les techniques d'analyse statique de code. L'analyse statique de programmes permet de prédire des comportements ou des ensembles de valeurs survenant à l'exécution, à partir du code source d'un programme. Le cours présentera des analyses de typage (plus ou moins élaborées), des analyses par interprétation abstraite. On s'intéressera non seulement à des analyses classiques comme le non débordement de tableau mais encore à des analyses de ressources plus spécifiques des systèmes embarqués. Ces analyses s'appuient sur une sémantique formelle du langage d'écriture des programmes.

Modalité d'évaluation

Examen (50%), examen de TP et/ou projets (50%).

Bibliographie

  • Glynn Winskel, : The Formal Semantics of Programming Languages, MIT Press, 1993
  • Benjamin C. Pierce : Types and Programming languages, MIT Press, 2002
  • Flemming Nielson, Hanne Riis Nielson, Chris Hankin, : Principles of programming analysis, Springer Verlag, 2005 94

Contact

EPN 05 Informatique
2 rue conté 31.1.79
75003 Paris
Tel :01 40 27 20 38
Agathe Froger

Voir les dates et horaires, les lieux d'enseignement et les modes d'inscription sur les sites internet des centres régionaux qui proposent cette formation