A Gitlab repository containing a collection of models that have been submitted as benchmark for the Model-Checking Contest, as well as scripts to generate new instances.

PaNDA-TPN is a formal verification tool for the state estimation, prognosis and diagnosability of time Petri nets (TPN).

RuDD is a Binary Decision Diagram (BDD) library written in pure Go. Freely available on GitHub.

Since 2018, we have been developing a novel approach to symbolic model checking for Petri nets, which we call polyhedral reduction. By “symbolic”, we mean a method that allows the exact representation of a system’s entire state space without having to enumerate each state individually in an exhaustive way.

Presentation on the advantages of using a formal-model execution engine to control and verify critical robotic systems

Our paper on the formal verification of autonomy in earth observation satellites has been accepted at the 10th International Congress and Exhibition on Embedded Real-Time Software and Systems (ERTSS 2020).

Our tool, TINA, won a gold medal in the “state space” category of the Model-Checking Contest 2020, an international competition of model-checking tools for the verification of concurrent systems. This is the second year in a row that TINA came first in the “state space” category.

A tool paper about MCC—our software for transformings models of High-Level Petri nets, given in PNML, into equivalent Place/Transition nets, not the competition!—has been accepted at Petri Nets 2020. You can find more about it here:

For the last 20 years, I have been developing my own “static site generators” in order to create pages for my personal website. Static site generator have many benefits when compared to Content Management Systems, especially in terms of security, but also because they are generally more “low maintenance”. Did I tell you that the last edit on my pages were in December 2015.

“Epoch avait un an ! Rome remplaçait Sparte …” I was born in France in 1971. I obtained my PhD from INRIA and the University of Nice - Sophia Antipolis in 1999, and I hold a Master’s Degree in computer science from École Normale Supérieure de Lyon, where I studied parallel programming and architecture. In 1993, I worked for one year on developing vision and learning algorithms for a smart retina for the French ministry of defence, then joined INRIA Sophia Antipolis for a PhD thesis on using mobile process calculi as a programming model.