Home > Verimag > Tools > Tools


Main Lab Tools

  • AMT 2.0 Analog Monitoring Tool

    AMT 2.0 is a tool for offline monitoring and measuring temporal specifications over discrete and continuous behaviors.

  • BIP Compiler

    The BIP compiler and execution engines for simulation, execution, exploration and debug of BIP models.

  • Pagai a static analyzer

    Pagai is a static analyzer based on the LLVM framework.

  • SASA a SimulAtor of Self-stabilizing Algorithms

    SASA is a Self-stabilizing Algorithms SimulAtor, based on the so-called Atomic State model (ASM) introduced by Dijkstra in its seminal article on Self-stabilizing distributed algorithms.

  • SpaceEx State Space Explorer

    The SpaceEx platform, a tool designed to facilitate the implementation of algorithms related to reachability and safety verification of continuous and hybrid systems.

  • the Chamois CompCert Compiler

    A version of the CompCert certified compiler with added optimizations and a backend for the Kalray KVX processor.

  • The Synchrone Reactive Toolbox

    This Toolbox consists of development tools targeting the design of reactive programs (typically, for critical embedded systems). It features the Lustre V6 language compiler and interpreter, the Lutin reactive system environment modeling language interpreter, the Lurette automated testing tool, the Lesar model-checker, the RDBG (Reactive Programs) debugger, and the gnuplot-rif and sim2chro data visualizers.


    • VPL (Verimag/Verified Polyhedron Library) [Open-source distribution, beta, basic maintenance]

      An abstract domain of convex polyhedra, formally verified in Coq for formally verified static analyzers, such as Verasco.

    • BDDC v2 [Binary distribution, basic maintenance]

      A command-line logical calculor, based on the Binary Decision Diagrams library of the Lustre compiler.

    • BIP-SMC : A Statistical Model Checking Engine for the BIP framework

      A statistical model checking engine prototype for the BIP framework.

    • d/dt [Privately distributed, beta, basic maintenance]

      d/dt is a prototype tool for reachability analysis of continuous and hybrid systems

    • FISSC Fault-injection and simulation secure collection (Verimag, CEA-Leti, Morpho)

      Fault-injection and simulation secure collection (Verimag, CEA-Leti, Morpho)

    • Lazart Source-level code robustness analysis against fault injection

      Source-level code robustness analysis against fault injection

    • Lutin [Open-source distribution, active maintenance]

      A (target) language for describing and simulating stochastic reactive systems.

      Lutin is now part of the Lustre V6 toolbox (lus2lic, lurette, rdbg)

    • Mjollnir

      A quantifier elimination tool

    • Montre A Tool for Monitoring Timed Regular Expressions [Open-source distribution, beta, basic maintenance]

      Montre is a monitoring tool to search patterns specified by timed regular expressions over real-time behaviors. It uses timed regular expressions as a compact, natural, and highly-expressive pattern specification language for monitoring applications involving quantitative timing constraints. The tool essentially incorporates online and offline timed pattern matching algorithms so it is capable of finding all occurrences of a given pattern over both logged and streaming behaviors. (…)

    • Multi-core interference Analysis [Binary distribution, beta, basic maintenance]

      A timing analysis tool for multi-core: From a description of data-flow application and initial schedule and mapping, it produces an updated schedule (release dates) that takes into account the inter-task interference. The focus is on the interference due to shared bus.


      This library provides an algorithmic infrastructure for reachability computation of non-linear dynamical systems.

    • ParetoLib Multidimensional Pareto Boundary Learning Library for Python [Open-source distribution, beta, active maintenance]

      This library implements an algorithm for learning the boundary between an upward-closed set X1 and its downward-closed component X2 (i.e., X=X1+X2). Generally, the library supports spaces X of dimension N. The algorithm selects sampling points x=(x1,x2,...,xN) for which it submits membership queries ’is x in X1?’ to an external Oracle. Based on the Oracle answers and relying on monotonicity, the algorithm constructs an approximation of the boundary, called the Pareto front. The algorithm (…)

    • Reglo [Binary distribution, basic maintenance]

      A compiler which translates regular expressions into either a set of language equations, or into a Lustre program.

    • RTD-Finder A COMPOSITIONAL VERIFICATION TOOL FOR Real-time BIP MODELS [Binary distribution, beta, basic maintenance]

      RTD-Finder tool implements a compositional method for the verification of component-based Real-time systems modeled in RT-BIP language. RTD-Finder verifies safety properties.

    • SatAns-Cert [Open-source distribution, pre-alpha, no maintenance]

      An OCaml wrapper certified in Coq to check answers of 2018 state-of-the-art SAT-solvers.

    • StreamExplorer [Binary distribution, pre-alpha, no maintenance]

      Dataflow multi-core scheduling using SMT solvers.

    • The Lustre V4 Toolbox [Binary distribution, basic maintenance]

      The Lustre Toolbox includes Lustre V4 and the model-checker Lesar.

    • The VPL Tactic [Open-source distribution, pre-alpha, no maintenance]

      A tactic for simplifying linear arithmetic within Coq goals, with oracles from the VPL library.


Initially developped at Verimag, the tools and prototypes below are now distributed elsewhere.
  • Aspic Accelerated Symbolic Polyhedral Invariant Computation

    This software is based on Linear Relation Analysis, and combines classic LRA (with widening) and acceleration techniques.

  • BinSec Binary code analysis for security

    BINSEC is an open-source toolset to help improve software security at the binary level. It relies on cutting-edge research in binary code analysis, at the intersection of formal methods, program analysis, security and software engineering. It is powered up by state-of-the-art techniques such as binary-level formal methods, symbolic execution, abstract interpretation, SMT solving and fuzzing. BINSEC has been successfully applied in a number of security-related contexts, such as (…)

  • GUEB Static analyzer for detection use-after-free vulnerabilities on binary code

    GUEB is a static analyzer performing use-after-free detection on binary. GUEB performs a value analysis on binary code, which tracks pointers and the states of the heap objects. When GUEB detects the use of a freed pointer, it extracts the sub-graph representation of the use-after-free.

  • LIBTLMPWT Model Power-Consumption and Temperature in SystemC/TLM

    Library for power consumption and thermal modeling.

  • Pinapa A front-end for SystemC/TLM

    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.

  • PinaVM

    SystemC front-end based on LLVM, and back-ends to generate code like Promela (input language for SPIN).

  • sc-during

    Library for parallel programming on top of SystemC


The tools below are prototypes or tools that are not active anymore.
  • aadl2sync [Binary distribution, pre-alpha, no maintenance]

    An AADL to synchronous programs translator

  • aadl4ocaml [Open-source distribution, pre-alpha, no maintenance]

    an ocaml library for parsing AADL code.

  • Argos and Larissa

    Argos is an automaton language, similar to StateCharts, but with synchronous semantics.

  • DFinder A Compositional Deadlock Detection and Verification Tool for BIP Models [Binary distribution, beta, no maintenance]

    D-Finder tool implements a compositional and incremental method for the verification of component-based systems described in BIP language encompassing multi-party interaction.

    For deadlock detection, D-Finder applies proof strategies to eliminate potential deadlocks by computing increasingly stronger invariants.

    Finally, the use of abstraction in invariant computation may introduce false positives. D-Finder proposes a refinement procedure to remove those cases for BIP programs with Boolean variables.


    FLATA is a tool for the analysis of non-deterministic linear integer programs (also known as counter automata).


    FLATA-C is static-analysis front-end, implemented as a FRAMA-C plugin, that aims at extracting Numerical Transition System models from C programs with low-level pointer updates such as e.g.: allocation, deletion, pointer arithmetic, etc. The generated NTS models can be used with off-the-shelf verifiers such as FLATA or ELDARICA. We target the following types of errors in the C code: null or dangling pointer dereferencing unaligned memory accesses memory leaks double free out-of-bound (…)

  • IF Toolset Intermediate Format and Verification Toolset [Open-source distribution,

    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 Invariants Verification System

    InVeSt is a tool for verification of invariance properties of infinite state systems.

  • Kronos [Binary distribution, beta, no maintenance]

    Kronos is a tool for model-checking of timed automata against specifications expressed using the real-time temporal logic TCTL.

  • L2CA a tool for the analysis of pointer programs

    Lists to Counter Automata: a tool for the analysis of pointer programs

  • OpenKronos [Privately distributed, pre-alpha, no maintenance]

    OpenKronos: is an on-the-fly verification tool for timed automata based on an integration of the DBM library of Kronos into CADP.

  • PHAVer [Binary distribution, pre-alpha, no maintenance]

    PHAVer is a tool for reachability analysis of continuous and hybrid systems based on Linear Hybrid Automata.

  • SCRV Runtime verification for SystemC/TLM designs

    SCRV allows to cover the non-determinism of the scheduling choices, when executing a SystemC/TLM model with the SystemC engine.

  • SMI Symbolic Model Interface

    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.

  • SR3 : Secure Resilient and Reputation-based Routing [Binary distribution, beta, no maintenance]

    SR3 is a many-to-one routing protocol, designed for wireless sensor networks, which is both secure and resilient. It is a reinforced random walk that is partially determinized using a reputation mechanism.

  • ss2lus Simulink/Stateflow to Lustre [Binary distribution, beta, no maintenance]

    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

    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.

Contact | Site Map | Site powered by SPIP 4.2.13 + AHUNTSIC [CC License]

info visites 4004411