My research focuses on theoretical aspects of software verification. More specifically I study the algebraic properties of various models of program behaviour. My interests also include logic, automata theory, mechanised proofs, concurrency theory and nominal mathematics. I have authored a number of papers in peerreviewed international conferences and journals on some of these topics.
Projects
Kleene Algebras with converse
Explore the converse operation on relations! Decide (in)equations!
Kleene lattices
This project focuses on the decidability of certain universal equations over binary relations.
Concurrent Kleene Algebras
CKA is a formalism that extends plain Kleene algebra with concurrent features. The goal is to reason about concurrency and concurrent programs in an algebraic, compositionnal fashion.
Language Algebras
This project focuses on the equational theory of algebras of languages, their decidability, complexity, and axiomatisations.
Nominal Algebras
In this project, we investigate how Kleene algebras may be enhanced with nominal features.
Coauthors
My research is the result of collaborations with many friends and colleagues. I have in particular written papers together with these people:
Damien Pous, Insa Stucke, Georg Struth, Tobias Kappé, Alexandra Silva, Bas Luttik, Fabio Zanasi, Daniela Petrişan, Jurriaan Rot, Jana Wagemaker, David Pym, Simon Docherty, James Brotherston, Nikos Gorogiannis, and Max Kanovich.
Featured papers: Full list of publications  
A Compositional Deadlock Detector for Android Java
(in ASE 2021)
with James Brotherston, Nikos Gorogiannis and Max Kanovich . 
More  
Partially Observable Concurrent Kleene Algebra
(in CONCUR 2020)
with Jana Wagemaker, Simon Docherty, Jurriaan Rot, Tobias Kappé and Alexandra Silva . 
More  
Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness
(in FoSSaCS 2020)
with Tobias Kappé, Alexandra Silva, Fabio Zanasi and Jana Wagemaker . 
More  
Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra
(in FSCD 2020)
with David Pym . 
More  
A Complete Axiomatisation of a Fragment of Language Algebra (in CSL 2020)  More  
A Kleene theorem for nominal automata
(in ICALP 2019)
with Alexandra Silva . 
More  
Featured talks: Full list of talks  
Avancées récentes sur les algèbres de Kleene concurrentes
séminaire du LACL
in Créteil,
December 2021
(in French)

More  
Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra
FSCD
in Paris,
July 2020

More  
Recent developments in concurrent Kleene algebra
Séminaire PPS
in Paris,
June 2020

More  
A complete axiomatisation of a fragment of language algebra
CSL
in Barcelona,
January 2020

More  
Pomsets with boxes: towards Atomic CKA
Highlights
in Warsaw,
September 2019

More  
A Kleene Theorem for Nominal Automata
ICALP
in Patras,
July 2019

More  
Pomset languages and concurrent Kleene algebras
Séminaire automates
in Paris,
November 2017

More  
The Equational Theory of Algebras of Languages
BLAST
in Nashville,
August 2017

More  
The Equational Theory of Positive Relation Algebra
MOVE
in Marseille,
March 2017

More  
Une introduction aux algèbres de Kleene
Inter'Actions
in Lyon,
May 2016
(in French)

More 