La vérification d'un système se réduit souvent au calcul de l'ensemble des états atteignables. En général, cet ensemble est infini car le système manipule des variables évaluées dans un domaine infini (des variables entières, des horloges, des files de communication, etc). Pour décrire et manipuler ces ensembles infinis, on utilise des représentations symboliques. Par exemple, pour les systèmes à compteurs, on considère des contraintes linéaires [CH-POPL78] ou des automates arithmétiques [BW-ICALP02], des automates représentant des langages réguliers de vecteurs d'entiers encodés par des mots de bits.
Pour obtenir la convergence du calcul itératif de l'ensemble des états atteignables, une des méthodes consiste à utiliser des techniques approchées permettant d'obtenir effectivement une sur approximation en un nombre fini d'itérations. Par exemple, dans le cas des polyèdres convexes, on pourra utiliser l'opérateur d'élargissement décrit dans [CH-POPL78], qui utilise la structure géométrique des ensembles représentés pour en donner une sur approximation.
Cette technique géométrique d'approximation des polyèdres n'a pas d'équivalent pour les automates arithmétiques. En utilisant la structure particulière des automates arithmétiques, exposée dans [L-TECH04], l'objectif du stage est d'étendre l'élargissement des polyèdres aux automates arithmétiques. Cette extension sera guidée par des expérimentations faites avec l'outil FAST disponible au sein de l'équipe.