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 peer-reviewed 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 | |