## Maître de conférences in LaBRI (University of Bordeaux)

I am maître de conférence in the university of Bordeaux, in the

Méthodes Formelles team of the

LaBRI.

In general, I am mainly interested in the study of subclasses of infinite graphs, their different presentations, the model-checking problem over them, and the languages they accept.
In particular, I worked on the class of graphs defined by higher-order stack tree rewriting systems, on the study of counter systems and their trace languages (for flat counter systems and vector addition systems), on the origin semantics of streaming string transducers, and on extensions of MSO over infinite words.

I am currently co-directing (at distance)

Prince Matthew, PhD student in IIT Goa (India) jointly with

Sreejith A.V..

With

Sreejith A.V. and

Meenakshi D’Souza, we are in charge of a project funded by CEFIPRA,

Verification of Adaptive Control Systems.

#### Main research interests:

- Infinite graphs
- Counter Systems
- Verification
- Automata theory
- Languages theory
- Higher-order systems

#### Software :

- Cairn, a tool for visualizing the execution of a parser (for compiling course).

#### Before that…

From September 2016 to July 2017 I was occupying a post-doc position (adiunkt naukowy) in the computer science institute of the University of Warsaw (MIMUW), where I was part of the project «A unified theory of finite-state recognisability» lead by Mikołaj Bojanczyk. In this project, I was working with Bruno Guillon, Laure Daviaud and Sreejith Ajithkumar Vijayalekshmi. We worked on the characterisation of graphs describing the origin semantics of streaming transducers (and their extensions), and on the decidability of logics over words (i.e. determine which predicate can be added to MSO/FO while retaining decidability).

From September 2015 to June 2016, I had a half-time ATER position in the Laboratoire d’Informatique Gaspard Monge (Champs-sur-Marne) until January, after which I visited Matthew Hague in the computer science department of the Royal Holloway university of London (Egham). We worked on extending verification techniques for higher order models to models which include an arborescent behaviour.

I did my PHD in the Laboratoire d’Informatique Gaspard Monge (Champs-sur-Marne) with Didier Caucal and Antoine Meyer.

### Adress :

LaBRI

Domaine Universitaire

351 cours de la Libération

33405 Talence

### Office :

307

### Phone :

(+33)6 31 30 63 80

### Email :

vincent.penelle [AT] labri [DOT] fr