L'analyse de systèmes (logiciels et matériels) est un thème 
de recherche très actif. Il est motivé par le besoin de disposer de 
méthodes et de techniques automatiques pour vérifier le bon 
fonctionnement de systèmes critiques dont les défaillances peuvent 
avoir des conséquences graves.

Typiquement un système est modélisé par un automate 
étendu par différentes sortes de variables et de structures 
de données. Des techniques d'analyse des configurations accéssibles 
dans ces modèles sont alors utilisées pour vérifier
que les spécifications sont bien satisfaites.

Dans ce contexte, les automates à compteurs (variables entières)
sont des modèles très courants. Cependant, l'analyse de tels 
modèles est complexe (et de manière générale, indécidable).

Le sujet de ce stage est d'étudier et d'implémenter des techniques 
permettant de construire des abstractions de ces modèles par des automates 
finis. De telles techniques permettent de réduire le problème
de l'analyse d'un automate à compteurs à celui d'un automate 
fini (plus abstrait).

Le travail comporte un travail bibliographique, suivi d'un travail de
réalisation et d'expérimentation.