Academic Homepage ^*

Contents

• 1 General Information
  • 1.1 Past Affiliations and Activities
  • 1.2 Publications and Supervisions
• 2 Miscellaneous Odds and Ends

1 General Information

I am an Associate Professor of Computer Science in the SDS team of the LIFO, teaching at the INSA CVL in Bourges.

My research interests fall mainly within the perimeter of “formal verification”, and include various aspects of automata and transducers theory, term rewriting, formal logic, and their applications.

Starting on April 15th, I supervise the Ph.D. thesis of Amine Rifi, Towards Formal Semantics and Proven Compliance of Business Workflows Processing Personal Data. It is directed by Sabine Frittella.

I supervised the CIFRE Ph.D. thesis of Adrien Jousse, defended on December 13, 2022, on the cybersecurity of automotive networks. The industrial partner for this thesis was the automotive supplier Valeo, where Benjamin Venelle supervised. It was directed by Christian Toinard.

I am head of “option 4AS” (Architecture, Administration, Audit, and Security Analysis) since 2021.

1.1 Past Affiliations and Activities

1.1.1 Inria Links, Lille, 2013–2017

I have been a member of the Inria team Links (formerly Mostrare), under the direction of Joachim Niehren, from October 2013 to August 2017, successively as a post-doctoral fellow, research engineer, and Temporary Research and Teaching Attaché (ATER), teaching at Lille 1. I worked within the ANR CoLiS.

1.1.2 University of Franche-Comté, VESONTIO, 2011–2013

I received my Ph.D. in Computer Science in 2013 from the University of Franche-Comté, working in the VESONTIO team of the DISC/LIFC department of the CNRS research institute FEMTO-ST (UMR 6174); I was also a member of the Inria/CASSIS team, and my Ph.D. was financed by the Inria and the Direction Générale de l’Armement (DGA).

Thesis title: Tree Automata, Approximations, and Constraints for Verification — Tree (Not Quite) Regular Model-Checking. Supervised by: Prs. Kouchnarenko and Héam. The manuscript can be downloaded below.

1.2 Publications and Supervisions

1.2.1 Supervised Ph.D. Thesis

1. Protection obligatoire vérifiée au regard des objectifs safety du secteur automobile
   co-authors: A. Jousse, C. Toinard, B. Venelle
   Supervised Ph.D. thesis  — Defended by Adrien Jousse on Dec 13, 2022
   

1.2.2 Published / Accepted Papers

1. Protecting Sensitive Data Against Deductions in Business Processes: Formal Semantics and Model-Checking
   co-authors: S. Frittella, A. Rifi
   International Conference SEFM2026 (preprint available)  — November 2026
   
2. SAT-Based Automated Completion for Reachability Analysis
   co-authors: Y. Boichut, A. Boiret
   International Conference CIAA 2024  — September 2024
   
3. A safe dynamic access control providing mandatory automotive cybersecurity
   co-authors: A. Jousse, C. Toinard, B. Venelle
   International Conference CSCI  — 2021
   
4. oMAC : Open Model for Automotive Cybersecurity
   co-authors: A. Jousse, C. Toinard, B. Venelle
   International Conference (Automotive Cyber Security) ESCAR  — 2019
   
5. Logics for Unordered Trees with Data Constraints
   co-authors: A. Boiret, J. Niehren, R. Treinen
   Elsevier — International Journal Journal of Computer and System Sciences  — January 2019
   
6. Equivalence of Symbolic Tree Transducers
   co-authors: A. Boiret, J. Niehren
   Springer LNCS – International Conference DLT’17  — August 2017
   
7. Automata for Unordered Trees
   co-authors: A. Boiret, J. Niehren, R. Treinen
   Elsevier — International Journal Information & Computation  — April 2017
   
8. The Emptiness Problem for Tree Automata with at Least One Disequality Constraint is NP-hard
   co-authors: P.C. Héam, O. Kouchnarenko
   Elsevier — International Journal Information Processing Letters.  — February 2017
   
9. Logics for Unordered Trees with Data Constraints on Siblings
   co-authors: A. Boiret, J. Niehren, R. Treinen
   Springer LNCS – International Conference LATA’15  — March 2015
   
10. Deterministic Automata for Unordered Trees
    co-authors: A. Boiret, J. Niehren, R. Treinen
    EPTCS – International Symposium GandALF’14  — July 2014
    
11. Loops and Overloops for Tree Walking Automata (Extended Version)
    co-authors: P.C. Héam, O. Kouchnarenko
    Elsevier – International Journal TCS  — December 2011 – March 2012
    Additional webpage and slides.
12. From Linear Temporal Logic Properties to Rewrite Propositions
    co-authors: P.C. Héam, O. Kouchnarenko
    Springer LNCS – International Conference IJCAR’12 (Long Paper)  — Jan 2012
    Corresponding slides.
    • Erratum: the translation rule (⊥) is obviously erroneous in this version. Refer to the updated paper.
13. On Positive TAGED with a Bounded Number of Constraints
    co-authors: P.C. Héam, O. Kouchnarenko
    Springer LNCS – International Conference CIAA’12 (Short Paper)  — March 2012
    Corresponding slides.
14. Loops and Overloops for Tree Walking Automata
    co-authors: P.C. Héam, O. Kouchnarenko
    Springer LNCS – International Conference CIAA’11 (Long Paper)  — March 2011
    Additional webpage and slides.
15. SAT Solvers for Queries over Tree Automata with Constraints
    co-authors: P.C. Héam, O. Kouchnarenko
    IEEE – International Workshop CSTVA’10  — January – April 2010
    Corresponding slides.

1.2.3 Thesis and Miscellaneous

1. Tree Automata, Approximations, and Constraints for Verification — Tree (Not Quite) Regular Model-Checking
   co-authors: supervisors: P.C. Héam, O. Kouchnarenko
   Ph.D. Thesis  — Sept 27, 2013
   Corresponding slides.
2. Random Generation of Positive TAGEDs wrt. the Emptiness Problem
   co-authors: P.C. Héam, O. Kouchnarenko
   INRIA Research Report  — November 2010
   Corresponding slides.
3. Algorithms for Tree Automata with Constraints
   co-authors: supervisors: P.C. Héam, O. Kouchnarenko
   M.Sc. Thesis  — July 2010
   Corresponding slides.

2 Miscellaneous Odds and Ends

• qtest: Inline unit tests extractor for OCaml projects
  qtest is part of the Batteries development platform for OCaml. Batteries uses qtest to extract and run its many (≈ 850) inline unit tests. qtest is not tied to Batteries however, and can be used with OCaml projects large and small. (note: here qtest refers to version 2 only – I didn’t write v1, and it has been phased out now).
• My Python implementation of nondeterministic finite automata
  This was not originally intended for public consumption at all, but I found it useful enough for pedagogical and research prototyping purposes.

  It consists in a very naive implementation of NFA and most algorithms thereon (determinisation, minimisation, language enumeration, morphisms, various kinds of products including parameterized synchronised product, CTL model-checking,...), graphviz/dot-based PDF visualisation, generation of LaTeX figures, conversion of regular expressions to automata,...

  Not yet available but somewhat planned: tree automata, term rewriting, LTL/CTL* model-checking.

  Given that what little documentation exists is interspersed with my teaching materials, and that it’s not coded with readability in mind, I don’t really expect it to be of much use to anyone who did not write it — I didn’t even bother giving it a name — but here it is.

*

This page was last updated on September 9, 2026.

This document was translated from L^AT_EX by H^EV^EA.