Jérôme LEROUX
Jérôme Leroux Directeur de Recherches (CNRS)

Équipe LaBRI : Méthodes formelles
Fonction administrative : Responsable Equipe Méthodes Formelles
Page personnelle : http://www.labri.fr/~leroux
Courrier électronique : jerome.lerouxarobaselabri.fr
Bureau : 264
Tél : +33 (0)5 40 00 35 09


Recherche

Mes travaux de recherche s'inscrivent dans le cadre de l'automatisation de la vérification des systèmes infinis.



La logique de Presburger est adaptée à l'analyse des systèmes à compteur. En effet cette logique est décidable (on peut décider la
satisfiabilité d'une formule) et permet de représenter des ensembles complexes, appelés ensembles de Presburger dans la suite.
On peut par exemple représenter des polyèdres non nécessairement convexes et des contraintes de modulo. Malheureusement,
en pratique les outils permettant de manipuler des ensembles de Presburger sont rapidement limités par la taille des
représentations symboliques implicitement calculées. Mes travaux de recherche dans l'automatisation de l'analyse des systèmes
à compteur s'orientent vers (1) le développement de nouvelles méthodes de résolution de la logique de Presburger en permettant
à terme de manipuler différentes représentations symboliques au sein d'un même solveur, et (2) le développement de nouvelles
méthodes de vérification basées sur des représentations symboliques pour la logique de Presburger, ou des sous classes de cette
logique.

Automates arithmétiques et logique de Presburger
Depuis 1969, nous savons que les automates arithmétiques permettent de représenter tout ensemble de Presburger. Alors qu'il
existe des algorithmes efficaces pour construire un automate arithmétique à partir d'une formule de Presburger, le problème
inverse de la synthèse d'une formule de Presburger à partir d'un automate représentant un ensemble de Presburger n'a été que
partiellement résolu par moi-même dans un article à INFINITY en 2003, Louis Latour (alors doctorant à Liège, Belgique) dans un
article à LICS en 2004 et par Denis Lugiez (CMI, Marseilles) dans un article à CIAA en 2004 pour des sous-classes restreintes
d'automates. Le problème de la synthèse est centrale pour développer de nouvelles représentations symboliques manipulant à la
fois des automates et des formules. Comme un automate arithmétique peut représenter des ensembles qui ne sont pas
définissables dans la logique de Presburger, le problème de la synthèse est naturellement lié à celui de décider si un automate
représente effectivement un ensemble de Presburger. Rappelons que ce problème est resté longtemps ouvert avant d'avoir été
résolu en 1991 par Muchnick, en temps quadruple-exponentiel. J'ai prouvé en 2004 que l'on pouvait décider en temps
polynômial si un automate représente un ensemble de Presburger. De plus, pour un tel automate, j'ai montré comment faire la
synthèse en temps polynômial. Ces résultats on été publiés dans un article à LICS en 2005. J'ai ensuite passé une grande partie
de l'année 2006 à rédiger un manuscrit détaillant ces résultats sur 134 pages. Pour simplifier la lecture de ce manuscrit, je
projette de le publier prochainement en plusieurs parties indépendantes. En 2008 en collaboration avec Gérald Point (Ingénieur
de recherche au LaBRI, Bordeaux) nous avons implémenté les algorithmes détaillés dans ce manuscrit dans l'outil Batof.
Cet outil permet de faire la synthèse en moins d'une minute pour des automates à plus de 100k états. Ces résultats
encourageant ont été publiés à la conférence internationale TACAS en 2009.


Représentations symboliques hétérogènes pour la logique de Presburger. Expérimentalement, grâce à l'API Genepi,
nous avons observé que les automates arithmétiques et les formules de Presburger fournissent deux
représentations symboliques efficace pour des sous-classes d'ensembles de Presburger incomparables. Pour combiner au mieux
ces deux représentations symboliques, je travaille sur le problème des représentations symboliques hétérogènes permettant de
combiner à la fois des automates et des formules. En 2009, en collaboration avec Florent Bouchy et Alain Finkel (LSV, ENS-
Cachan) nous avons publiés des premiers résultats sur ce problème au workshop international TIME. En 2009, en collaboration
avec Bernard Boigelot et Julien Brusten (Liège, Belgique) nous avons publiés d'autres résultats sur ce thème à la conférence
internationale CADE. Dans cette publication nous avons montré une extension au théorème de Cohbam révélant la structure
interne des composantes fortement connexe d'un automate arithmétique. De cette structure nous avons déduit une
représentation hétérogène combinant formules et automates. Prochainement, nous développerons des méthodes et outils pour
manipuler directement cette nouvelle représentation.



Accessibilité pour les réseaux de Petri. Le problème de l'accessibilité pour les réseaux de Petri est resté ouvert
de nombreuses années avant d'être montré décidable en 1980. L'algorithme décidant cette propriété est complexe et l'on ne peut
en déduire qu'une borne non-élémentaire de complexité. Depuis cette date, différentes présentations plus simples de cet
algorithme on été publiées mais aucun vrai nouvel algorithme n'a été trouvé. En 2009, j'ai publié un article à la conférence
internationale LICS montrant qu'une configuration finale n'est pas accessible depuis une configuration initiale si et seulement s'il
existe un invariant inductif définissable dans la logique de Presburger contenant la configuration initiale et ne contenant pas la
configuration finale. De ce résultat théorique, on déduit un algorithme très simple à implémenter pour décider l'accessibilité dans
les réseaux de Petri. En effet, il suffit d'énumérer pour chaque entier positif $k$ les états accessibles en au plus $k$ transitions et
les formules de Presburger de longueur $k$. Si pendant l'énumération des configurations accessibles, on découvre la
configuration finale, l'algorithme termine en décidant l'accessibilité. Si pendant l'énumération des formules de Presburger on
obtient une formules dénotant un invariant inductif contenant la configuration initiale et ne contenant pas la configuration finale,
l'algorithme termine en décidant la non-accessibilité. Bien que cet algorithme soit simple à implémenter, la complexité de
l'accessibilité dans les réseaux de Petri reste ouverte. De plus, un tel algorithme ne pourra pas être utilisé en pratique car étant
par nature énumératif il a peu de chance de terminer en un temps raisonnable. Néanmoins l'existence d'invariant inductif
définissable dans la logique de Presburger permet d'envisager de nouveaux algorithmes utilisant la logique de Presburger pour
abstraire des ensembles de configurations d'un réseau de Petri.

Extrait de publications











Responsabilité pédagogique

Pendant deux ans (2006-2008), j'ai donné un cours de 4H dans le master Science et Techologies, en spécialité Ingénierie des
systèmes critiques, dans l'UE Technologie de la vérification. Pendant ce cours je présentais quelques méthodes permettant de
vérifier à l'aide de représentations symboliques des systèmes infinis. Depuis 2008, je donne un cours de 16H dans le master
Science et Technologies, en spécialité Ingénierie des systèmes critiques, dans l'UE Formalisme et Description de Système. Dans
cette UE de 48H, plusieurs méthodes pour vérifier des logicielles sont présentées. Dans la partie dont je suis responsable, je
présente essentiellement deux méthodes CEGAR (à la Clarke et à la McMillan).

Administration

Je suis responsable pour le LaBRI du projet ANR Averiss de l'appel à projet ANR SETIN, édition 2006. Ce projet regroupe
le LSV (ENS de Cachan), le LiAFA (Univ. Paris 7) et le LaBRI (Univ. Bordeaux 1), et vise à développer des méthodes pour la
vérification de logiciels. Le LaBRI a obtenu 170 Euros répartie en 40 Keuros de fonctionnement, 40 Keuros de matériel et 90
Keuros pour une bourse de thèse.

Depuis 2010 : chef d'équipe adjoint "Méthode Formelle".

2009-2010 : membre CC du Labri

Pendant l'année 2008-2009, j'ai participé à deux comités de sélections pour des postes de maître de conférence à l'université de
Paris 7 et l'université de Paris 12.

Pendant les 2 années 2006-2008, j'ai été membre de la commission de spécialiste de l'université de Bordeaux 1 en section 27.

Depuis janvier 2006, je suis responsable du séminaire hebdomadaire MVTSI de mon équipe présenté à
http://www.labri.fr/groupes.

Comité de programme & Comité d'organisation

2009, membre du comité de programmes du workshop international "INFINITY"

Diffusion

2006 : comité d'organisation de l'école d'été MOVEP'06 http://movep.labri.fr.

Valorisation

2009-2011 : BINCOA, ANR Arpege, participant
2007-2009 : SPACIFY, ANR TL, participant
2007-2009 : AVERISS, ANR SETIN, coordinateur local, 170 KE
2003-2006 : PERSEE, ACI Sécurité Informatique, particpant

Expertise

J'ai participé à la sélection de publications pour plusieurs conférences internationales.
2009 : Rapporteur prix de thèse IBM - avis (Belgique)


Page mise à jour le 13/08/2010 à 10:56