Sémantique, typage et analyse de programme

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