[hal] [dblp] [scholar]
The iFinder tool for auto-generation of invariants and compositional verification of BIP systems.
The IF (Intermediate Format) Toolbox for model-checking of timed asynchronous systems.
The SDL2IF translator module for TASTE/SDL components into IF.
The FLATA tool for analysis of counter automata systems.
The L2CA (Lists to Counter Automata) Tool for extracting counter automata models from programs operating on single-linked lists.
The PDG (Probabilistic Decision Graphs) Package, an implementation of the idea presented in the CAV'99 paper "On the representation of Probabilities over Structured Domains"
The MDD (Multivalued Decision Diagrams) Package, an implementation of MDDs with binary branching on conditions of the form "variable <= value", a promising idea I have developed during my DEA on symbolic representations for model checking
For my colleagues at Verimag only, the Intranet/Administrative web and database.
Last updated 09-12-2023