Analyse des Programmes

Le service de formation continue de l’UPMC figure parmi les premiers centres de formation continue universitaire en France. Son offre complète de formations lui permet d’apporter une réponse adaptée et personnalisée aux besoins des professionnels, des entreprises, collectivités et administrations. Sémantiques des programmes séquentiels :
Sémantique opérationnelle. Typage, classage et sousclassage.
Modèles des langages de programmation et sémantique dénotationnelle. Sémantique relationnelle, logique de Hoare.

Sémantiques des programmes concurrents :
Rappels sur les automates. Les systèmes de transition.
Logiques temporelles, modales. Les calculs de processus et les équivalences observationnelles. Réseaux de Pétri.
Application aux structures de concurrence présentes dans les langages (Ada, java etc.) ou les systèmes.

Analyse statique de programmes :
Analyse statique et interprétation abstraite, analyses dataflow. Graphe de contrôle, de dépendances, d'appels, forme SSA. Applications à la sûreté de fonctionnement.
Vérification de contraintes de typage : le bytecode verifier de Java. Application à la détection d' étreintes fatales
(deadlocks). Applications à la sécurité. Analyse d'alias.
Analyse interprocédurale. Débogage abstrait, coupes dynamiques (dynamic slicing).


Test :
Techniques de tests : graphes de commande, graphes de transaction, flots de données, tests aux limites, tests syntaxiques. Outils de mise en oeuvre et de génération de tests. Limites actuelles des tests.

Vérification :
On étudiera quelques outils de vérification par modèles (PROD,SPIN par exemple) et quelques outils d'analyse de programmes.