Explore projects

C++17 library for LTL, ω-automata manipulation, and model checking. Comes with Python bindings.

Clojure implementation of rational type expressions

The point of this tool is to learn a Pomset Recognizer (PR) or a Tree Automaton (TA, not implemented yet) by querying a Minimally Adequate Teacher (MAT). For more details, please read the companion article: https://arxiv.org/abs/2501.03914

The point of this tool is to learn a Computation Tree Logic (CTL) formula that separates a set of positive and negative Kripke structures, i.e. is verified by the former but not the latter. For more details, please read the companion article: http://arxiv.org/abs/2402.06366

Web server for Spot

Online application for rewriting LTL formula or translating them into automata.

LDNS is a DNS library that facilitates DNS tool programming

Dockerfiles for constructing build environments for Spot

Builds the docker image that runs on spot-sandbox.lrde.epita.fr.