
---
  title: "The Equational Theory of Positive Relation Algebra"
  venue: "MOVE"
  location: "Marseille"
  month: 3
  year: 2017
  link: "http://pageperso.lif.univ-mrs.fr/~benjamin.monmege/seminaireMOVE/"
  slides: "move-03-17.pdf"
  featured: true
  excerpt: >
    Algebras of relations appear naturally in many contexts, in computer science as well as in mathematics. They constitute a framework well suited to the semantics of imperative programs. Kleene algebras are a starting point: these algebras enjoy very strong decidability properties, and a complete axiomatisation. The goal of this talk was to export known results from Kleene algebra to some of its extensions.

    We first consider a known extension: Kleene algebras with converse. Decidability of these algebras is already known, but the algorithm witnessing this result was too complicated to be practical. We propose a simpler algorithm, which is more efficient, and whose correctness is easier to establish. It allows us to prove that this problem lies in the complexity class PSpace-complete.

    Then we study Kleene allegories. Few results were known about this extension. Following results about closely related algebras, we establish the equivalence between equality in Kleene allegories and the equality of certain sets of graphs. We then develop a new automaton model (so-called Petri automata), based on Petri nets. We prove the equivalence between the original problem and comparing these automata. In the restricted setting of identity-free Kleene lattices, we also provide an algorithm performing this comparison. This algorithm uses exponential space. However, we prove that the problem of comparing Petri automata lies in the class ExpSpace- complete.

    
---
---
  title: "A formal exploration of Nominal Kleene Algebra"
  venue: "MFCS"
  location: "Krakow"
  month: 8
  year: 2016
  link: "http://mfcs.ki.agh.edu.pl/"
  slides: "mfcs-08-16.pdf"
  featured: false
  excerpt: >
    An axiomatisation of Nominal Kleene Algebra has been proposed by Gabbay and Ciancia, and then shown to be complete and decidable by Kozen et al. However, one can think of at least four different formulations for a Kleene Algebra with names: using freshness conditions or a presheaf structure (types), and with explicit permutations or not. We formally show that these variations are all equivalent. Then we introduce an extension of Nominal Kleene Algebra, motivated by relational models of programming languages. The idea is to let letters (i.e., atomic programs) carry a set of names, rather than being reduced to a single name. We formally show that this extension is at least as expressive as the original one, and that it may be presented with or without a presheaf structure, and with or without syntactic permutations. Whether this extension is strictly more expressive remains open. All our results were formally checked using the Coq proof assistant.
---
---
  title: "Une introduction aux algèbres de Kleene"
  venue: "Inter'Actions"
  location: "Lyon"
  month: 5
  year: 2016
  link: "https://interactions16.sciencesconf.org/"
  slides: "interactions-05-16.pdf"
  remark: "in French"
  featured: true
  excerpt: >
    Une algèbre de Kleene est une structure algébrique munie des opérations de expressions régulières: zéro, un, somme, produit et étoile. Les relations binaires forment une telle algèbre, ainsi que les langages. Cette théorie est décidable, c'est à dire qu'il existe un algorithme permettant de décider si une équation utilisant uniquement ces opérations est une loi universelle des algèbres de Kleene. Ceci a plusieurs applications. 1) Il est assez naturel de modéliser une instruction d'un programme par une relation entre états mémoire. Cette abstraction permet de plonger les programmes dans une algèbre de Kleene relationnelle. Ainsi, on peut tester dans certains cas si deux programmes sont équivalents en utilisant cette théorie. 2) Dans une preuve mathématique manipulant des relations binaires, on peut faire appel à cet algorithme pour automatiser certaines étapes de preuve. Diverses extensions de ces algèbres existent, certaines étant mieux comprises que d'autres.
---
---
  title: "Petri automata for Kleene Allegories"
  venue: "LiCS"
  location: "Kyoto"
  month: 7
  year: 2015
  link: "http://lics.rwth-aachen.de/lics15/"
  slides: "lics-07-15.pdf"
  featured: false
  excerpt: >
    Kleene algebra axioms are complete with respect to both language models and binary relation models. In particular, two regular expressions recognise the same language if and only if they are universally equivalent in the model of binary relations.

    We consider Kleene allegories, i.e., Kleene algebras with two additional operations which are natural in binary relation models: intersection and converse. While regular languages are closed under those operations, the above characterisation breaks. Instead, we give a characterisation in terms of languages of directed and labelled graphs. We then design a finite automata model allowing to recognise such graphs, by taking inspiration from Petri nets.

    This model allows us to obtain decidability of identity-free relational Kleene lattices, i.e., the equational theory generated by binary relations on the signature of regular expressions with intersection, but where one forbids unit. This restriction is used to ensure that the corresponding graphs are acyclic. The decidability of graph-language equivalence in the full model remains open.
---
---
  title: "Kleene Algebra with Converse"
  venue: "RAMiCS"
  location: "Marienstatt"
  month: 4
  year: 2014
  link: "http://mathcs.chapman.edu/ramics2014/"
  slides: "ramics-28-04-14.pdf"
  featured: false
  excerpt: >
    The equational theory generated by all algebras of binary relations with operations of union, composition, converse and reflexive transitive closure was studied by Bernátsky, Bloom, Ésik, and Stefanescu in 1995. We reformulate some of their proofs in syntactic and elementary terms, and we provide a new algorithm to decide the corresponding theory. This algorithm is both simpler and more efficient; it relies on an alternative automata construction, that allows us to prove that the considered equational theory lies in the complexity class PSpace.

    Specific regular languages appear at various places in the proofs. Those proofs were made tractable by considering appropriate automata recognising those languages, and exploiting symmetries in those automata.

    
---
---
  title: "The Equational Theory of Algebras of Languages"
  venue: "BLAST"
  location: "Nashville"
  month: 8
  year: 2017
  link: "https://my.vanderbilt.edu/blast2017/"
  slides: "blast-08-17.pdf"
  featured: true
  excerpt: >
    We investigate the equational theory of algebras of formal languages with the constants empty language and unit language, the unary mirror image and Kleene star operators, and the binary operations of union, intersection and concatenation. We start by reducing the problem of deciding the validity of an equation over this signature to the equality of certain graph languages. This allows us to derive decidability, and to show that this problem is in fact ExpSpace-complete. Using this graph characterisation, and removing the Kleene star from our signature, we then propose a complete finite axiomatisation of this theory. This development was obtained using the proof assistant Coq.
---
---
  title: "On Decidability of Concurrent Kleene Algebra"
  venue: "CONCUR"
  location: "Berlin"
  month: 9
  year: 2017
  link: "https://www.concur2017.tu-berlin.de/"
  slides: "concur-09-17.pdf"
  featured: false
  excerpt: >
    Concurrent Kleene algebras support equational reasoning about computing systems with concurrent behaviours. Their natural semantics is given by series(-parallel) rational pomset languages, a standard true concurrency semantics, which is often associated with processes of Petri nets. We use constructions on Petri nets to provide two decision procedures for such pomset languages motivated by the equational and the refinement theory of concurrent Kleene algebra. The contribution to the first problem lies in a much simpler algorithm and an ExpSpace complexity bound. Decidability of the second, more interesting problem is new and, in fact, ExpSpace-complete.

    
---
---
  title: "The theory of languages"
  venue: "Highlights"
  location: "London"
  month: 9
  year: 2017
  link: "http://highlights-conference.org/london/"
  slides: "brunet-highlights-09-17.pdf"
  featured: false
  excerpt: >
    We investigate the equational theory of algebras of formal languages with the constants empty language and unit language, the unary mirror image and Kleene star operators, and the binary operations of union, intersection and concatenation. We start by reducing the problem of deciding the validity of an equation over this signature to the equality of certain graph languages. This allows us to derive decidability, and to show that this problem is in fact ExpSpace-complete. Using this graph characterisation, and removing the Kleene star from our signature, we then propose a complete finite axiomatisation of this theory. This development was obtained using the proof assistant Coq.
---
---
  title: "The Equational Theory of Algebras of Languages"
  venue: "PPLV Seminar"
  location: "London"
  month: 4
  year: 2017
  link: "http://pplv.cs.ucl.ac.uk"
  slides: "pplv-04-17.pdf"
  featured: false
  excerpt: >
    We investigate the equational theory of algebras of formal languages with the constants empty language and unit language, the unary mirror image and Kleene star operators, and the binary operations of union, intersection and concatenation. We start by reducing the problem of deciding the validity of an equation over this signature to the equality of certain graph languages. This allows us to derive decidability, and to show that this problem is in fact ExpSpace-complete. Using this graph characterisation, and removing the Kleene star from our signature, we then propose a complete finite axiomatisation of this theory. This development was obtained using the proof assistant Coq.
---
---
  title: "Algèbres de Relations, Étude des algèbres de Kleene avec converse"
  location: "Paris"
  month: 9
  year: 2013
  slides: "internship_M2-09-13.pdf"
  remark: "Internship defence, in French"
  featured: false
---
---
  title: "Deciding Kleene Algebra with converse is PSpace-complete"
  venue: "GeoCal"
  location: "Bordeaux"
  month: 3
  year: 2014
  link: "http://perso.ens-lyon.fr/olivier.laurent/geocal/"
  slides: "geocal-25-03-14.pdf"
  featured: false
---
---
  title: "Décidabilité des Treillis de Kleene sans identité"
  venue: "JFLA"
  location: "Val d'Ajol"
  month: 1
  year: 2015
  link: "http://jfla.inria.fr/2015/index.html"
  slides: "jfla-01-15.pdf"
  remark: "in French"
  featured: false
  excerpt: >
    Families of binary relations are important interpretations of regular expressions, and the equivalence of two regular expressions with respect to their relational interpretations is decidable: the problem reduces to the equality of the denoted regular languages.

    Putting together a few results from the literature, we first make explicit a generalisation of this reduction, for regular expressions extended with converse and intersection: instead of considering sets of words (i.e., formal languages), one has to consider sets of directed and labelled graphs.

    We then focus on identity-free regular expressions with converse—a setting where the above graphs are acyclic—and we show that the corresponding equational theory is decidable. We achieve this by defining an automaton model, based on Petri Nets, to recognise these sets of acyclic graphs, and by providing an algorithm to compare such automata.
---
---
  title: "Decidability of Identity-free Kleene Lattices"
  venue: "LAC"
  location: "Chambéry"
  month: 11
  year: 2014
  link: "https://lama.univ-savoie.fr/~hirschowitz/LAC2014/"
  slides: "lac-11-14.pdf"
  featured: false
  excerpt: >
    Families of binary relations are important interpretations of regular expressions, and the equivalence of two regular expressions with respect to their relational interpretations is decidable: the problem reduces to the equality of the denoted regular languages.

    Putting together a few results from the literature, we first make explicit a generalisation of this reduction, for regular expressions extended with converse and intersection: instead of considering sets of words (i.e., formal languages), one has to consider sets of directed and labelled graphs.

    We then focus on identity-free regular expressions with converse—a setting where the above graphs are acyclic—and we show that the corresponding equational theory is decidable. We achieve this by defining an automaton model, based on Petri Nets, to recognise these sets of acyclic graphs, and by providing an algorithm to compare such automata.
---
---
  title: "Deciding Kleene Algebra with converse is PSpace-complete"
  venue: "PACE"
  location: "Lyon"
  month: 2
  year: 2014
  link: "http://perso.ens-lyon.fr/daniel.hirschkoff/pace/pg-feb14.html"
  slides: "pace-09-02-14.pdf"
  featured: false
---
---
  title: "Equivalence of regular expressions with converse on relations"
  venue: "PiCoq"
  location: "Lyon"
  month: 6
  year: 2013
  slides: "picoq-06-13.pdf"
  featured: false
---
---
  title: "The Equational Theory of Algebras of Languages"
  venue: "RAMiCS"
  location: "Lyon"
  month: 5
  year: 2017
  link: "http://www.ens-lyon.fr/LIP/PLUME/RAMiCS17/index.html"
  slides: "ramics-05-17.pdf"
  remark: "Special session on mechanised reasoning"
  featured: false
  excerpt: >
    We investigate the equational theory of algebras of formal languages with the constants empty language and unit language, the unary mirror image and Kleene star operators, and the binary operations of union, intersection and concatenation. We start by reducing the problem of deciding the validity of an equation over this signature to the equality of certain graph languages. This allows us to derive decidability, and to show that this problem is in fact ExpSpace-complete. Using this graph characterisation, and removing the Kleene star from our signature, we then propose a complete finite axiomatisation of this theory. This development was obtained using the proof assistant Coq.
---
---
  title: "The Equational Theory of Positive Relation Algebra"
  venue: "PACE"
  location: "Shanghai"
  month: 11
  year: 2016
  link: "http://perso.ens-lyon.fr/daniel.hirschkoff/pace/pg-nov16.html"
  slides: "pace-11-16.pdf"
  featured: false
  excerpt: >
    Algebras of relations appear naturally in many contexts, in computer science as well as in mathematics. They constitute a framework well suited to the semantics of imperative programs. Kleene algebras are a starting point: these algebras enjoy very strong decidability properties, and a complete axiomatisation. The goal of this talk was to export known results from Kleene algebra to some of its extensions.

    We first consider a known extension: Kleene algebras with converse. Decidability of these algebras is already known, but the algorithm witnessing this result was too complicated to be practical. We propose a simpler algorithm, which is more efficient, and whose correctness is easier to establish. It allows us to prove that this problem lies in the complexity class PSpace-complete.

    Then we study Kleene allegories. Few results were known about this extension. Following results about closely related algebras, we establish the equivalence between equality in Kleene allegories and the equality of certain sets of graphs. We then develop a new automaton model (so-called Petri automata), based on Petri nets. We prove the equivalence between the original problem and comparing these automata. In the restricted setting of identity-free Kleene lattices, we also provide an algorithm performing this comparison. This algorithm uses exponential space. However, we prove that the problem of comparing Petri automata lies in the class ExpSpace- complete.

    
---
---
  title: "A Kleene Theorem for Petri automata"
  venue: "Highlights"
  location: "Brussels"
  month: 9
  year: 2016
  link: "http://highlights-conference.org/brussels/"
  slides: "pbrunet-highlight16-slides.pdf"
  featured: false
  excerpt: >
    Petri Automata are automata based on Petri nets, whose operational semantics is designed to recognise sets of graphs. We introduced them in a recent paper [1] with Pous to study Kleene Allegory (KAl) expressions: terms built from a finite alphabet of variables, with the constants 0 and 1, the unary operators converse and Kleene star, and the binary operators union, composition and intersection. To any such expression, one can associate a set of graphs such that two expressions are universally equivalent when interpreted as binary relations if and only if their associated sets of graphs are equal. In [1] we gave a method to build from any Kleene Allegory expression a Petri automaton recognising the appropriate set of series parallel graphs. It is then natural to wonder what is the class of graph languages recognised by Petri automata. For the usual notion of finite state automata, the well known Kleene Theorem states that the languages recognisable by automata are exactly those specifiable by regular expressions. This year we provided a similar theorem for Petri automata and Kleene Allegory expressions [2]. Indeed the graph languages specified by Petri automata are precisely the languages denoted by KAl. Moreover, this entails that decidability of the equational theory of Kleene Allegories is equivalent to that of language equivalence for Petri automata. This decidability problem is still open. It is worth mentioning that the technical part of the proof in [2] actually uses a smaller syntax than Kleene Allegories, without converse nor identity. In this fragment the considered graphs are series-parallel, so that the key technical result is actually a Kleene theorem for series-parallel regular expressions and languages. References: 

    [1] Paul Brunet and Damien Pous. Petri automata for Kleene allegories. In Logic in Computer Science (LICS), 2015 30th Annual ACM/IEEE Symposium on, pages 68–79, July 2015. 

    [2] Paul Brunet. Algebras of relations: from algorithms to formal proofs. PhD Thesis, October 2016.
---
---
  title: "Petri automata for Kleene allegories"
  venue: "Rapido"
  location: "Paris"
  month: 6
  year: 2015
  link: "https://www.irif.fr/~saurin/RAPIDO/"
  slides: "slides-rapido-06-15.pdf"
  featured: false
  excerpt: >
    Kleene algebra axioms are complete with respect to both language models and binary relation models. In particular, two regular expressions recognise the same language if and only if they are universally equivalent in the model of binary relations.

    We consider Kleene allegories, i.e., Kleene algebras with two additional operations which are natural in binary relation models: intersection and converse. While regular languages are closed under those operations, the above characterisation breaks. Instead, we give a characterisation in terms of languages of directed and labelled graphs. We then design a finite automata model allowing to recognise such graphs, by taking inspiration from Petri nets.

    This model allows us to obtain decidability of identity-free relational Kleene lattices, i.e., the equational theory generated by binary relations on the signature of regular expressions with intersection, but where one forbids unit. This restriction is used to ensure that the corresponding graphs are acyclic. The decidability of graph-language equivalence in the full model remains open.
---
---
  title: "Petri automata for Kleene allegories"
  venue: "Midlands Graduate School"
  location: "Sheffield"
  month: 4
  year: 2015
  link: "http://staffwww.dcs.shef.ac.uk/people/G.Struth/mgs2015/mgs.html"
  slides: "slides-mgs-04-15.pdf"
  featured: false
  excerpt: >
    Kleene algebra axioms are complete with respect to both language models and binary relation models. In particular, two regular expressions recognise the same language if and only if they are universally equivalent in the model of binary relations.

    We consider Kleene allegories, i.e., Kleene algebras with two additional operations which are natural in binary relation models: intersection and converse. While regular languages are closed under those operations, the above characterisation breaks. Instead, we give a characterisation in terms of languages of directed and labelled graphs. We then design a finite automata model allowing to recognise such graphs, by taking inspiration from Petri nets.

    This model allows us to obtain decidability of identity-free relational Kleene lattices, i.e., the equational theory generated by binary relations on the signature of regular expressions with intersection, but where one forbids unit. This restriction is used to ensure that the corresponding graphs are acyclic. The decidability of graph-language equivalence in the full model remains open.
---
---
  title: "Pomset languages and concurrent Kleene algebras"
  venue: "Séminaire automates"
  location: "Paris"
  month: 11
  year: 2017
  link: "https://www.irif.fr/seminaires/automates/index"
  slides: "automates-11-17.pdf"
  featured: true
  excerpt: >
    Concurrent Kleene algebras (CKA) and bi-Kleene algebras support equational reasoning about computing systems with concurrent behaviours. Their natural semantics is given by series(-parallel) rational pomset languages, a standard true concurrency semantics, which is often associated with processes of Petri nets.

    In the first part of the talk, I will present an automaton model designed to describe such languages of pomset, which satisfies a Kleene-like theorem. The main difference with previous constructions is that from expressions to automata, we use Brzozowski derivatives.

    In a second part, I will use Petri nets to reduce the problem of containment of languages of pomsets to the equivalence of finite state automata. In doing so, we prove decidabilty as well as provide tight complexity bounds.

    I will finish the presentation by briefly presenting a recent proof of completeness, showing that two series-rational expressions are equivalent according to the laws of CKA exactly when their pomset semantics are equal.

    Joint work with Damien Pous, Georg Struth, Tobias Kappé, Bas Luttik, Alexandra Silva, and Fabio Zanasi.
---
---
  title: "Pomset languages and concurrent Kleene algebra"
  venue: "Theory seminar - QMU"
  location: "London"
  month: 2
  year: 2018
  link: "http://theory.eecs.qmul.ac.uk/seminars/"
  slides: "qmu-02-18.pdf"
  featured: false
  excerpt: >
    Concurrent Kleene algebras (CKA) and bi-Kleene algebras support equational reasoning about computing systems with concurrent behaviours. Their natural semantics is given by series(-parallel) rational pomset languages, a standard true concurrency semantics, which is often associated with processes of Petri nets.

    In the first part of the talk, I will present a recent proof of completeness, showing that two series-rational expressions are equivalent according to the laws of CKA exactly when their pomset semantics are equal. 

    In a second part, I will use Petri nets to reduce the problem of containment of languages of pomsets to the equivalence of finite state automata. In doing so, we prove decidability as well as provide tight complexity bounds.

    Joint work with Damien Pous, Georg Struth, Tobias Kappé, Alexandra Silva, and Fabio Zanasi
---
---
  title: "Bracket Algebra"
  venue: "Highlights"
  location: "Berlin"
  month: 9
  year: 2018
  link: "http://highlights-conference.org"
  slides: "highlights-09-18.pdf"
  featured: false
  excerpt: >
    Nominal techniques have received a lot of attention in recent years, as they describe in a simple yet precise manner phenomena related to variable renaming, like alpha-equivalence, scopes, locality... However, they seem to suffer from two shortcomings: they are not yet able to handle interleaved scopes, and do not apply well to relational semantics of programs. In this talk I will describe an ongoing project to provide an algebraic treatment of the semantics of programming languages which contain explicitly allocation and de-allocation binders, inspired by previous work of Gabbay, Ghica and Petrişan. I will present the initial setup, defining a notion of alpha-equivalence of traces, and briefly describe how this may be extended to regular languages. I will present some decidability results we obtained, and hint at future investigations. Most of these developments have been formalised in Coq. This is joint work with Alexandra Silva and Daniela Petrisan.
---
---
  title: "A Kleene Theorem for Nominal Automata"
  venue: "ICALP"
  location: "Patras"
  month: 7
  year: 2019
  link: "https://icalp2019.upatras.gr"
  slides: "brunet-icalp-2019.pdf"
  featured: true
  excerpt: >
    Nominal automata are a widely studied class of automata designed to recognise languages over infinite alphabets. In this paper, we present a Kleene theorem for nominal automata by providing a syntax to denote regular nominal languages. We use regular expressions with explicit binders for creation and destruction of names and pinpoint an exact property of these expressions - namely memory-finiteness - identifying a subclass of expressions denoting exactly regular nominal languages.
---
---
  title: "Pomsets with boxes: towards Atomic CKA"
  venue: "Highlights"
  location: "Warsaw"
  month: 9
  year: 2019
  link: "http://highlights-conference.org/"
  slides: "brunet-highlights-2019.pdf"
  featured: true
  excerpt: >
    Concurrent Kleene Algebra (CKA) was introduced by Hoare, Moeller, Struth and Wehrman in 2009 as a compositional framework to reason about concurrent programs. Their free model is given by series(-parallel) rational pomset languages, a standard true concurrency semantics. A key feature of CKA is provided by the weak exchange law, allowing one to partially interleave threads. For instance this enables one to consider that a specification that allows for three parallel threads can be refined in an implementation on two processors, provided all the dependencies required in the specification are satisfied.

    However, when trying to use this framework to model realistic programs, this law is often too permissive. By allowing every possible interleaving, one cannot for example provide mutual exclusion guarantees. To try and address this issue while retaining the good properties of CKA (compositionality, decidability, applicability…) we modify the underlying model of pomsets to include so-called “boxes”. Boxes intuitively correspond to an “atomic{…}” construct in a parallel programming language: they isolate part of the program from interference from the rest of the concurrent environment.

    In future work, we plan to develop logics — in the style of van Benthem, Hennessy, and Milner — for describing the properties of CKA models. Here we identify three key challenges: first, to establish appropriate operational/algebraic—logical equivalence theorems; second, to establish logical characterizations of the role of boxes in specifying behaviour; third, identification of local reasoning principles, such as ‘frame rules’, that will support compositional formal reasoning about properties of CKA models. 

    In this talk, I will present this new model of pomsets with boxes, together with semantic and axiomatic ways of reasoning about them. This is joint work with David Pym, and all the results have been verified using the proof assistant Coq.
---
---
  title: "A complete axiomatisation of a fragment of language algebra"
  venue: "CSL"
  location: "Barcelona"
  month: 1
  year: 2020
  link: "https://www.eacsl.org/?page_id=62"
  slides: "brunet-csl-2020.pdf"
  featured: true
  excerpt: >
    We consider algebras of languages over the signature of reversible Kleene lattices, that is the regular operations (empty and unit languages, union, concatenation and Kleene star) together with intersection and mirror image. We provide a complete set of axioms for the equational theory of these algebras. This proof was developed in the proof assistant Coq.
---
---
  title: "Recent developments in concurrent Kleene algebra"
  venue: "Séminaire PPS"
  location: "Paris"
  month: 6
  year: 2020
  link: "https://www.irif.fr/seminaires/pps/index"
  slides: "brunet-pps-2020.pdf"
  featured: true
  excerpt: >
    Concurrent Kleene algebra (CKA) is an algebraic framework to reason about concurrent programs. In recent years, we have studied several ways of enhancing CKA with extra features, to carry out more sophisticated verification tasks.

    In this talk, I will start by recalling the basic definitions of CKA, and its decidability and completeness theorems. We will then take an overview of some of its extensions, considering aspects such as control-flow, memory consistency and mutual exclusion.

    This talk is the result of collaborations with Tobias Kappé, Jana Wagemaker, Simon Docherty, Fabio Zanasi, Jurriaan Rot, Alexandra Silva, David Pym, Damien Pous, and Georg Struth.
---
---
  title: "Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra"
  venue: "FSCD"
  location: "Paris"
  month: 7
  year: 2020
  link: "https://fscd2020.org/"
  slides: "brunet-fscd-2020.pdf"
  featured: true
  excerpt: >
    Concurrent Kleene Algebra is an elegant tool for equational reasoning about concurrent programs. An important feature of concurrent programs that is missing from CKA is the ability to restrict legal interleavings. To remedy this we extend the standard model of CKA, namely pomsets, with a new feature, called boxes, which can specify that part of the system is protect from outside interference. We study the algebraic properties of this new model. Another drawback of CKA is that the language used for expressing properties of programs is the same as that which is used to express programs themselves. This is often too restrictive for practical purposes. We provide a logic, `pomset logic', that is an assertion language for specifying such properties, and which is interpreted on pomsets with boxes. We develop the basic metatheory for the relationship between pomset logic and CKA, including frame rules to support local reasoning, and illustrate this relationship with simple examples.
---
---
  title: "Recent developments in concurrent Kleene algebra"
  venue: "IRIS scientific meeting"
  location: "London"
  month: 12
  year: 2020
  slides: "brunet-iris-2020.pdf"
  featured: false
  excerpt: >
    Concurrent Kleene algebra (CKA) is an algebraic framework to reason about concurrent programs. In recent years, we have studied several ways of enhancing CKA with extra features, to carry out more sophisticated verification tasks.

    In this talk, I will start by recalling the basic definitions of CKA, and its decidability and completeness theorems. We will then take an overview of some of its extensions, considering aspects such as control-flow, memory consistency and mutual exclusion.

    This talk is the result of collaborations with Tobias Kappé, Jana Wagemaker, Simon Docherty, Fabio Zanasi, Jurriaan Rot, Alexandra Silva, David Pym, Damien Pous, and Georg Struth. 
---
---
  title: "Avancées récentes sur les algèbres de Kleene concurrentes"
  venue: "séminaire LIRICA"
  location: "Marseille"
  month: 1
  year: 2021
  link: "https://www.lis-lab.fr/lirica/"
  slides: "brunet-lirica-2021.pdf"
  remark: "in French"
  featured: true
---
---
  title: "Avancées récentes sur les algèbres de Kleene concurrentes"
  venue: "Séminaire ACADIE"
  location: "Toulouse"
  month: 4
  year: 2021
  link: "https://www.irit.fr/en/departement/dep-reliability-systems-and-software/acadie-team/"
  slides: "brunet-n7-2021.pdf"
  featured: false
---
---
  title: "Observations and locality in distributed processes"
  venue: "IRIS scientific meeting"
  location: "London"
  month: 3
  year: 2021
  link: "https://uclirisproject.wordpress.com/"
  featured: false
---
---
  title: "Avancées récentes sur les algèbres de Kleene concurrentes"
  venue: "Séminaire LOVE"
  location: "Paris"
  month: 1
  year: 2021
  link: "https://lipn.univ-paris13.fr/en/love-logics-and-verification/"
  slides: "brunet-lipn-2021.pdf"
  featured: false
---
---
  title: "Avancées récentes sur les algèbres de Kleene concurrentes"
  venue: "Séminaire MAREL"
  location: "Montpellier"
  month: 4
  year: 2021
  link: "http://www.lirmm.fr/recherche/equipes/marel"
  slides: "brunet-lirmm-2021.pdf"
  featured: false
---
