École Jeunes Chercheurs en Programmation - INRIA Sophia Antipolis - 17 au 28 Mars 1997

Analyse sémantique de programmes par interprétation abstraite (Droits d'auteurs/Copyright Notice)
Patrick Cousot
Jeudi 20 Mars 1997, 9h15 - 12h30 & 14h30 - 17h45.

Introduction à l'interprétation abstraite (transparents)

• Introduction informelle et exemples ;
• Rappels mathématiques sur les treillis et points fixes ;
• Approximation de points fixes par correspondances de Galois ;
• Approximation de points fixes par élargissement/rétressissement ;
• Méthode de conception d'une interprétation abstraite.

Exemples d'analyse sémantique de programmes

• Analyse de nécessité (strictness analysis) pour les programmes fonctionnels du premier ordre (transparents) ;
• Analyse de programmes logiques basée sur des contraintes ensemblistes ;
• Typage et inférence de types par interprétation abstraite (transparents) ;
• Vérification de modèle (model-checking) et interprétation abstraite (transparents).