a:2:{s:2:"fr";s:1902:"Ma recherche concerne la vérification des programmes et de systèmes concurrents en utilisant comme formalisme pivot les réseaux de Petri et leurs abréviations. Nous suivons, dans l'équipe que j'anime avec Claude Kaiser, deux axes complémentaires : Le premier axe aborde directement les problèmes de conception et de vérification d'applications concurrentes écrites dans des langages de haut niveau en particulier dans langage Ada95. Une part de ces travaux, vise à étudier et à comparer la sémantique de ces langages pour la conception d'applications concurrentes. Ces travaux sont fait plus particulièrement avec Claude Kaiser et Pierre Rousseau qui travaille sur les méthodes de découpe ("slicing") de programmes concurrents et qui est l'auteur de l'outil Yasnost. Le second axe concerne les techniques d'analyse structurelles des réseaux de Petri et leur adaptation aux réseaux de haut niveau en particulier dans le cadre de la vérification de programmes concurrents ; ces techniques sont dites « structurelles » car elles se basent sur la structure du modèle et non sur l'analyse explicite de ses états accessibles. Parmi les résultats récents, nous pouvons citer l'élaboration de nouvelles réductions structurelles qui permettent de transformer des séquences d'actions non atomiques en une unique action atomique réduisant drastiquement le nombre d'états à analyser ou la définition de nouvelles techniques de stockage d'états, les "Delta-Marking", ou encore la parallélisation d'algorithmes de "model-checking". Ces travaux sont menés avec Sami Evangelista qui est l'auteur de l'outil Helena (http://helena.cnam.fr) et Christophe Pajault qui développe l'outil Cyclades. L'ensemble de ses travaux a donné lieu à l'outil Quasar (http://quasar.cnam.fr), outil de vérification automatique de programmes Ada concurrents. ";s:2:"en";s:1902:"Ma recherche concerne la vérification des programmes et de systèmes concurrents en utilisant comme formalisme pivot les réseaux de Petri et leurs abréviations. Nous suivons, dans l'équipe que j'anime avec Claude Kaiser, deux axes complémentaires : Le premier axe aborde directement les problèmes de conception et de vérification d'applications concurrentes écrites dans des langages de haut niveau en particulier dans langage Ada95. Une part de ces travaux, vise à étudier et à comparer la sémantique de ces langages pour la conception d'applications concurrentes. Ces travaux sont fait plus particulièrement avec Claude Kaiser et Pierre Rousseau qui travaille sur les méthodes de découpe ("slicing") de programmes concurrents et qui est l'auteur de l'outil Yasnost. Le second axe concerne les techniques d'analyse structurelles des réseaux de Petri et leur adaptation aux réseaux de haut niveau en particulier dans le cadre de la vérification de programmes concurrents ; ces techniques sont dites « structurelles » car elles se basent sur la structure du modèle et non sur l'analyse explicite de ses états accessibles. Parmi les résultats récents, nous pouvons citer l'élaboration de nouvelles réductions structurelles qui permettent de transformer des séquences d'actions non atomiques en une unique action atomique réduisant drastiquement le nombre d'états à analyser ou la définition de nouvelles techniques de stockage d'états, les "Delta-Marking", ou encore la parallélisation d'algorithmes de "model-checking". Ces travaux sont menés avec Sami Evangelista qui est l'auteur de l'outil Helena (http://helena.cnam.fr) et Christophe Pajault qui développe l'outil Cyclades. L'ensemble de ses travaux a donné lieu à l'outil Quasar (http://quasar.cnam.fr), outil de vérification automatique de programmes Ada concurrents. ";}