Vincent Penelle

Maître de conférences au LaBRI (Université de Bordeaux)

image

Je suis maître de conférences à l’université de Bordeaux depuis le 01 septembre 2017, au sein de l’équipe Méthodes Formelles du LaBRI.
Je suis responsable des parcours «Algorithme et Modèles» et «Vérification logicielle» du Master Informatique (de l’université de Bordeaux, bien entendu).
D’une manière générale, je m’intéresse aux graphes infinis (certaines sous-classes), à leurs différentes représentations, à leur problème de vérification de modèle, et aux langages qu’ils reconnaissent. En particulier, j’ai eu l’occasion de travailler sur la classe de graphes liés aux systèmes de réécriture d’arbres de piles, aux systèmes à compteurs et à leurs langages de traces (notamment aux systèmes à compteurs plats et aux systèmes d’addition de vecteurs), à la sémantique avec origine des transducteurs à registres et à des extensions de MSO sur les mots infinis.

Je co-encadre actuellement (à distance) Prince Matthew, doctorant à l’IIT Goa (Inde) avec Sreejith A.V..
Avec Sreejith A.V. et Meenakshi D’Souza, nous sommes porteurs d’un projet financé par le CEFIPRA, Verification of Adaptive Control Systems.

Intérêts principaux :

  • Graphes infinis
  • Systèmes à compteurs
  • Vérification
  • Théorie des automates
  • Théorie des langages
  • Systèmes d’ordre supérieur

Production logicielle :

  • Cairn, un outil de visualisation d’exécution de parseur (pour un cours de compilation).

Autrefois

.
De septembre 2016 à juillet 2017, j’étais post-doctorant (adiunkt naukowy) à l’institut d’informatique de l’Université de Varsovie (MIMUW), où je participais au projet «A unified theory of finite-state recognisability» mené par Mikołaj Bojanczyk. Dans le cadre de ce projet, je travaillais avec Bruno Guillon, Laure Daviaud et Sreejith Ajithkumar Vijayalekshmi. Nous avons travaillé sur la caractérisation des graphes décrivant la sémantique avec origine des streaming transducers (et leurs extensions), et sur la décidabilité de logiques sur les mots (c’est-à-dire déterminer quels prédicats on peut ajouter à MSO/FO en restant décidable).
De septembre 2015 à juin 2016 j’ai effectué un demi-ATER au Laboratoire d'Informatique Gaspard Monge, à Champs-sur-Marne, jusqu’en janvier, puis j’ai fait une visite de recherche au département d’informatique de la Royal Holloway university of London, à Egham, pour mener une collaboration avec Matthew Hague portant sur les extension des techniques de vérification sur des modèle d’ordre supérieur à des modèle faisant intervenir un comportement arborescent.
J’ai fait ma thèse au laboratoire d’informatique Gaspard Monge, à Champs-sur-Marne, sous la direction de Didier Caucal et d'Antoine Meyer.

Adresse :

LaBRI
Domaine Universitaire
351 cours de la Libération
33405 Talence

Bureau :

307

Téléphone :

(+33)6 31 30 63 80

Email :

vincent.penelle [AT] labri [DOT] fr