next up previous contents
suivant: COT : Composants et test monter: Présentation des modules précédent: A2R : analyse, synthèse et   Table des matières

Sous-sections

SAP : Sémantique et analyse de programmes

Présentation

Ce module présente les principales idées et méthodes utilisées en sémantique et analyse de programme. Une sémantique définit formellement le sens des programmes. Elle permet d'éviter les ambiguïtés, de prouver la correction de la mise en oeuvre ou de raisonner sur les programmes. L'analyse de programme est un type de raisonnement fondé sur une sémantique. Les analyses permettent de déduire automatiquement et statiquement des propriétés sur les programmes. Elles sont largement utilisés dans les phases de mise au point (découverte d'erreurs) et de compilation (optimisations).

Le domaine couvert fait partie des fondements des langages de programmation. Le module est de ce fait d'intérêt général ; il n'est lié ni à une équipe de recherche, ni à un langage particulier.

Plan du module

1.
Sémantiques opérationnelles. Sémantique à grands pas (naturelle). Sémantique à petits pas (SOS). Techniques de preuves.
2.
Analyse de flot de données. Exemples. Graphe de flot de contrôle. Treillis et points fixes. Résolution d'équations et de contraintes.
3.
Sémantiques dénotationnelles. Ordres partiels complets (CPO) et points fixes. Techniques de preuves.
4.
Interprétation abstraite - théorie de l'approximation statique. Treillis de propriétés. Connexion de Galois et approximation de points fixes. Analyse de signes.

5.
Systèmes de types.
6.
Interprétation abstraite - théorie de l'approximation dynamique. Élargissement et séquences descendantes. Analyse d'intervalles. Autres exemples d'analyse de variables numériques et hiérarchie d'interprétations abstraites. Analyse interprocédurale.
7.
Présentation d'articles de recherche récents.

Bibliographie

next up previous contents
suivant: COT : Composants et test monter: Présentation des modules précédent: A2R : analyse, synthèse et   Table des matières