Ahmed BOUAJJANI

Statut

Professeur des universités

Promotion

Membre honoraire 2013

Établissement

Université Paris Cité

Secteur disciplinaire

Sciences et Technologies de l'Information et de la Communication

Spécialité

Informatique

Thématique

► Vérification formelle de systèmes
► Analyse et vérification de programmes
► Automates et logique

Présentation

Le domaine de recherche d’Ahmed Bouajjani est celui de la vérification formelle des systèmes informatiques par des approches algorithmiques qui s’apparentent au model checking.
Au cours de sa carrière, Ahmed Bouajjani a cherché à pousser les limites de la vérification automatique au-delà des systèmes ayant un nombre fini de configurations. Ahmed Bouajjani s’est intéressé en particulier à la vérification de programmes en tenant compte de différents aspects tels que la manipulation de structures de données complexes, la récursivité, la concurrence, la création dynamique de processus, etc.
Ses travaux portent sur (1) la définition de formalismes basés sur la logique et les automates pour la modélisation et la description des propriétés de ces systèmes, (2) l’étude des propriétés de ces formalismes du point de vue de l’expressivité, de la décidabilité, et de la complexité, et (3) le développement d’algorithmes de vérification basés sur ces formalismes. Parmi les contributions d’Ahmed Bouajjani, on peut citer : algorithmes basés sur les
automates pour la vérification de modèles de programmes procéduraux et/ou concurrents/communicants, le développement de l’approche dite de « Regular Model Checking » pour la vérification de systèmes infinis, et l’étude de logiques et de méthodes d’analyse pour la vérification de programmes avec structures de données dynamiques.
Le projet actuel d’Ahmed Bouajjani vise à développer de nouvelles méthodes algorithmiques et techniques pour la vérification, la détection d’erreurs, et la correction de systèmes concurrents et distribués. Ce projet est motivé par l’important développement des architectures multi-coeurs et des infrastructures distribuées pour le « cloud computing ».