The tool LASH is developed in Liège. It allows analysis of extended automata, such as automata with counters and clocks, using automata-based symbolic representation structures (NDD, RVA). Acceleration techniques are used in order to help termination of the computation of reachability sets. The techniques used in LASH are based on the concept of meta-transition corresponding to computing (in one step) the effect of iterating an arbitrary number of times a sequence of actions (a control loop).
The tool TReX is developed in Paris (UP7) and in Grenoble (UJF). This tool allows the analysis of extended automata manipulating clocks and integer counters with parametric guards, communicating through shared variables and unbounded FIFO channels. TReX allows the construction of the reachability sets and finite abstract models of the analyzed systems. TReX uses PDBMs to represent sets of integer and real vectors, and it allows to manipulate nonlinear arithmetical constraints. TReX uses accurate extrapolation techniques to accelerate fixpoint calculations during the reachability analysis.
Both tools, LASH and TReX are interfaced with the common model description language IF.