FAST: acceleration from theory to practice |
| |
Authors: | Sébastien Bardin Alain Finkel Jérôme Leroux Laure Petrucci |
| |
Affiliation: | (1) LSL (LIST, CEA), Saclay, France;(2) LSV (UMR CNRS 8643, ENS de Cachan), Cachan, France;(3) LaBRI (UMR CNRS 5800, ENSEIRB, Université Bordeaux-1), Bordeaux, France;(4) LIPN (UMR CNRS 7030, Université Paris-13), Villetaneuse, France |
| |
Abstract: | Fast acceleration of symbolic transition systems (Fast) is a tool for the analysis of systems manipulating unbounded integer variables. We check safety properties by computing the reachability set of the system under study. Even if this reachability set is not necessarily recursive, we use innovative techniques, namely symbolic representation, acceleration and circuit selection, to increase convergence. Fast has proved to perform very well on case studies. This paper describes the tool, from the underlying theory to the architecture choices. Finally, Fast capabilities are compared with those of other tools. A range of case studies from the literature is investigated. This paper is mainly based on results presented at CAV 2003, TACAS 2004 and ATVA 2005. |
| |
Keywords: | Counter systems Infinite reachability set Symbolic representation Acceleration |
本文献已被 SpringerLink 等数据库收录! |
|