Tools developed in Verimag
An AADL to synchronous programs translator
an ocaml library for parsing AADL code.
Argos is an automaton language, similar to StateCharts, but with synchronous semantics.
A Binary Decision Diagrams library, initially written for the Lustre compiler in the early 90s.
The BIP toolset includes translators from various programming modes into BIP, source-to-source transformers as well as a compiler for generating code executable by a dedicated engine.
d/dt is a prototype tool for reachability analysis of continuous and hybrid systems
FLATA is a tool for the analysis of non-deterministic linear integer programs (also known as counter automata).
The IF Intermediate Representation based on extending communicating timed automata has been defined for being able to offer a powerful toolset offering simulation, analysis and verification facilities for different modelling languages for distributed real-time systems.
InVeSt is a tool for verification of invariance properties of infinite state systems.
Kronos is a tool for model-checking of timed automata against specifications expressed using the real-time temporal logic TCTL.
Lists to Counter Automata: a tool for the analysis of pointer programs
Library for power consumption and thermal modeling.
Lurette is an Automatic Test Generator for Reactive Programs.
A (target) language for describing and simulating stochastic reactive systems.
A quantifier elimination tool
This library provides an algorithmic infrastructure for reachability computation of non-linear dynamical systems.
Pagai is a static analyzer based on the LLVM framework.
PHAVer is a tool for reachability analysis of continuous and hybrid systems based on Linear Hybrid Automata.
Pinapa is a front-end for SystemC/TLM, that allows to combine the information on the architecture of a TLM platform, with the syntax trees of the threads.
A compiler which translates regular expressions into either a set of language equations, or into a Lustre program.
Library for parallel programming on top of SystemC
SCRV allows to cover the non-determinism of the scheduling choices, when executing a SystemC/TLM model with the SystemC engine.
The Symbolic Model Interface (SMI) is a library which provides for the efficient construction and manipulation of symbolic representations for finite state systems, in particular for communication protocols.
The main objective of this project is to allow the translation of Simulink/Stateflow (trademarks of The Mathworks Inc.) into the synchronous programming language Lustre allowing its associated compilers, model-checkers and abtract interpretation tools to be applied to Simulink designs.
TGV (Test Generation with Verification technology) is a tool for the generation of conformance test suites for protocols. It is the result of a collaboration of the project Pampa of the Irisa institute with the projet Spectre/INRIA of the Verimag research center.
The Lustre Toolbox includes Lustre V4 and the model-checker Lesar.
Lustre V6 is the last version of the academic Lustre compiler, featuring an ada-like package mechanism, structured data-types (enums, structures), array iterators, and static recursion.