Description
FLATA is a toolset for the manipulation and the analysis of non-deterministic integer programs (also known as counter automata). The input to the tool is a textual description of a counter automaton (see examples below).
The main functionalities of FLATA are:
- checking emptiness of the model, i.e. deciding if a final state is reachable from an initial state
- reducing the size of the input model to smaller models with equivalent emptiness problems
Download
FLATA is a free software under LGPL license. The current distribution of FLATA is available here: flata.tgz
A good way to get started using FLATA is to go through one of the following examples linked here: flata-examples.tgz
Installation
Prerequisites:
- JAVA version 1.6.0 or later
- YICES has to be installed in your executable path
- ANTLR has to be installed in your JAVA classpath
Run FLATA as e.g.
java -classpath flata.jar:antlr-3.2.jar verimag.flata.Main -ia synlifo.ca
See the README file for further information.
Documentation
The following papers are related to the FLATA project:
- M. Bozga, R. Iosif and F. Konecny. Fast Acceleration of Ultimately Periodic Relations VERIMAG TR-2010-3
- M. Bozga, C. Girlea and R. Iosif. Iterating Octagons TACAS 2009
- M. Bozga, R. Iosif and Y. Lakhnech Flat Parametric Counter Automata Fundamenta Informaticae, Volume 91 (2), 275 - 303, IOS Press (2009)
A white paper describing the functionalities of the toolset, and including a detailed description of the input syntax and options will be coming soon.
Extensions
It is possible to use FLATA in order to solve the satisfiability problem for SIL (Singly Indexed Logic), a logic used to specify properties of integer arrays. The extension can be downloaded here:
A description of the SIL logic and its applications can be found in the following papers:
- P. Habermehl, R. Iosif, T. Vojnar. A Logic of Singly Indexed Arrays LPAR’08
- M. Bozga, P. Habermehl, R. Iosif, F. Konecny, T. Vojnar. Automatic Verification of Integer Array Programs CAV’09
Contributors
- Marius Bozga (VERIMAG, Grenoble, France)
- Radu Iosif (VERIMAG, Grenoble, France)
- Tomas Vojnar (Brno University of Technology, Czech Republic)
- Filip Konecny (VERIMAG and Brno University of Technology)
Acknowledgements
This work was supported by the French national project ANR-09-SEGI-016 VERIDYC, by the Czech Science Foundation (projects P103/10/0306 and 102/09/H042), the Czech Ministry of Education (projects COST OC10009 and MSM 0021630528), and the internal FIT BUT grant FIT-S-10-1.
