Official LSV Web Site

FAST - Fast Acceleration of Symbolic Transition systems

[   News   |   Introduction   |   Related Tools   |   References   |   Experiments   |   Installation   |   Team   ]



Model-checking is a wide-spread technique in critical systems verification. Several efficient model-checkers are available. However, most of these tools are restricted to finite systems whereas many real systems are infinite, because of parameters or unbounded data structures.

FAST is a tool dedicated to the analysis of infinite systems. It performs automatic verification of systems augmented with (unbounded) integer variables. The main issue addressed by FAST is the computation of the exact (infinite) set of configurations reachable from a given set of initial configurations. Although such sets are in general not computable, FAST uses a semi-algorithm which is expected to terminate in most practical cases.

The techniques used in FAST are based on acceleration, which involves computing the effect of iterating a control loop of arbitrary length. FAST is also the first tool to use an heuristics to find automatically the good cycles to accelerate (in other accelerated symbolic model-checkers, the user has to provide such cycles). The models FAST operates on are composed of a finite control structure, guards are Presburger formulae, and operations affine functions. The user can provide a strategy to direct the reachability set computation. Strategies are written in a high-level language, which supports, for the moment, forward and backward reachability as well as more advanced constructs such as incremental sub-model analysis.

FAST has been applied to a large number of examples, ranging from tricky academic puzzles to communication protocols or multi-threaded JAVA programs. These examples are available here. In about 80% of these case studies the reachability set could effectively be computed using a forward algorithm and a basic predefined strategy. More elaborate strategies or a backward algorithm can lead to a considerable drop in computation time for some protocols.

FAST inputs and outputs.

Comparison with other tools

Other tools exist for the verification of unbounded counter automata. The following table shows a comparison between FAST and some of these tools. The main advantages of FAST are that FAST: For more details, see here .




Flattable systems




FAST team


About LSV