FAST: acceleration from theory to practice

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

• Type: Journal
• Year: 2008
• Where: STTT
• Authors: Sébastien Bardin, Alain Finkel, Jérôme Leroux, Laure Petrucci
• Keywords: Case Studies, Reachability, STTT 2008, Tools