LIAFA.

Au LIAFA, le projet s'intègre dans l'équipe Modélisation et Vérification dirigée par Paul Gastin. Cette équipe s'est élargie de manière significative ces dernières années entre autres autour d'un thème de recherche portant sur la ``Vérification de systèmes infinis : analyse qualitative et quantitative de systèmes logiciels'' et mené par Ahmed Bouajjani.

L'objectif de ce thème de recherche est de développer des techniques algorithmiques avancées pour la vérification automatique de systèmes complexes, en visant en particulier le domaine des protocoles de télécommunication et celui des systèmes logiciels embarqués.

Les directions de travail concernant ce thème de recherche sont les suivantes:

1. étude des modèles pemettant de capturer des aspects essentiels dans les comportements de systèmes complexes (manipulation de données sur des domaines infinis, contraintes temps-réel, paramétrisation, dynamisme de la mémoire et du contrôle, etc.),
2. étude de la décidabilité de problèmes de vérification pour des classes significatives de modèles,
3. développement d'algorithme d'analyse d'accessibilité basée sur des représentations symboliques d'ensembles (infinis) de configurations, et de procédures efficaces de constructions des espaces de configurations accessibles,
4. développement d'outils implémentant nos techniques de vérification, et leur utilisation pour le traitement d'études de cas non triviales.

Ainsi, le sujet de recherche de cette ACI se trouve au coeur de l'un des principaux thèmes de recherche de l'équipe ``Modélisation et Vérification'' du LIAFA.