Home > Teams > RSD > Tools > Tools



  • BIP Compiler [Binary distribution, active maintenance]

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

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

    A statistical model checking engine prototype for the BIP framework.

  • 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.


The tools below are prototypes or tools that are not active anymore.
  • 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 Intermediate Format and Verification Tool set

    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.

  • L2CA a tool for the analysis of pointer programs

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

  • 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.

The Verimag Tools page

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

info visites 1692352