Module VA : Méthodes de vérification automatique

Module VA : Méthodes de vérification automatique

Equipe pédagogique :

Nicolas Halbwachs, Suzanne Graf, Laurent Mounier

Volume :

24h.

Spécialité :

S&L

Ce module s'intéresse aux méthodes et outils de vérification et d'analyse automatiques. Une première partie concerne les méthodes de vérification des systèmes finis, applicables aux systèmes qui peuvent être modélisés comme des systèmes de transitions à nombre finis d'états. On s'intéresse à la spécification de ces systèmes (spécification opérationnelles -- à l'aide d'un autre système de transitions -- ou logiques -- en particulier à l'aide de logiques temporelles) et aux techniques et outils de vérification, attaquant en particulier le problème des systèmes à très grand nombre d'états (vérification à la volée, vérification symbolique). Dans une deuxième partie, on étudie les méthodes d'analyse fondées sur l'interprétation abstraite. Une des ambitions de ce module est de traiter le domaine depuis la théorie jusqu'aux problèmes de réalisation d'outils.

• Problèmatique de la vérification. Systèmes de transitions. Spécifications opérationnelles et logiques. Sémantiques linéaire et arborescente
• Comparaison de systèmes de transitions. Simulations et bisimulations.
• Logique temporelle linéaire et automates de Büchi
• Logique arborescente
• Interprétation abstraite: théorie et applications

Module VA : Méthodes de vérification automatique