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].
Les méthodes de vérifications basées sur des calculs symboliques se classent naturellement en deux familles: celles basées sur des calculs exacts et celles basées sur le raffinement d'abstractions. Ces deux familles de méthodes sont complémentaires. Les premières permettent de calculer, par une itération croissante, l'ensemble X des états atteignables. Les secondes sont guidées par la propriété à vérifier, et calculent, par une itération décroissante, une approximation supérieure suffisamment précise de X. Utilisées séparément, ces techniques ne permettent pas, en général, d'analyser des systèmes complexes de grande taille. Aussi, notre objectif consiste à réduire l'écart entre ces méthodes, en proposant notamment des techniques permettant de maîtriser l'imprécision lors des calculs approchés [GH-SAS06]. Nos premiers travaux dans ce sens cherchent à calculer de façon exacte le plus petit point fixe dans un treillis abstrait, ou en d'autres termes le plus petit invariant inductif représentable par un état abstrait. Le degré de précision est ainsi fixé par le choix du treillis abstrait (par exemple les intervalles, les octogones, les octaèdres, etc), et le calcul de plus petit point fixe est réalisé par des techniques de calculs symboliques. Dans cette approche, les techniques de raffinement pourraient s'appuyer sur les travaux existant dans le raffinement de domaines abstraits.
L'objectif du stage est d'identifier des classes de systèmes et de treillis abstraits supportant des méthodes de calcul symbolique exactes.
Ce stage pourra être poursuivi par une thèse.