Flata

Error creating thumbnail: /bin/bash: line 1: /usr/bin/convert: No such file or directory

Error code: 127

FLATA is a toolset for the manipulation and the analysis of non-deterministic integer programs (also known as counter automata). The main functionalities of FLATA are:

• reachability analysis of non-recursive programs -- deciding if an error state is reachable from an initial state

• termination analysis of non-recursive programs -- computation of termination preconditions

• computation of summaries of recursive programs

Running FLATA

Download

FLATA is a free software under LGPL license. The current distribution of FLATA is available here: flata.tgz

Prerequisites:

• JAVA version 1.6.0 or later

• YICES has to be installed in your executable path

• ANTLR and NTS has to be installed in your JAVA classpath

Run

A good way to get started using FLATA is to go through one of the examples (a subset of NTS benchmarks that FLATA can veriify) linked here: benchmarks.tgz

The input to the tool is a textual description of a counter automaton (see examples below), essentially a control flow.

Run FLATA as e.g.

java -classpath flata.jar:nts.jar:antlr-3.2.jar verimag.flata.Main VHDL/synlifo.correct.nts

See the README file for further information.

Verification of Non-recursive Programs

Reachability Analysis

FLATA compu

The core of the analysis is an algorithm from CAV'10.

Documentation

The following papers are related to the FLATA project:

A white paper describing the functionalities of the toolset, and including a detailed description of the input syntax and options will be coming soon.

Contributors

• Marius Bozga (VERIMAG, Grenoble, France)
• Radu Iosif (VERIMAG, Grenoble, France)
• Filip Konecny (VERIMAG and Brno University of Technology)
• Tomas Vojnar (Brno University of Technology, Czech Republic)

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.

Reference test

This is the text that you are going to verify with a reference.<ref>Reference details go here</ref>

References

<ref name="cav10">[seplogic.pdf Fast Acceleration of Ultimately Periodic Relations.] M. Bozga, R. Iosif, and F. Konecny. In Proc. of CAV'10, volume 6174 of LNCS, pages 227-242, 2010. Springer-Verlag. </ref>

<ref name="tacas12">[seplogic.pdf Deciding Conditional Termination.] M. Bozga, R. Iosif, and F. Konecny. In Proc. of TACAS'12, volume 7214 of LNCS, pages 252-266, 2012. Springer-Verlag. </ref>

<ref name="tacas13">[seplogic.pdf Underapproximation of Procedure Summaries for Integer Programs.] P. Ganty, R. Iosif and F. Konecny. In Proc. of TACAS'13. To appear. </ref>

<ref name="fm12">[seplogic.pdf A Verification Toolkit for Numerical Transition Systems.] H. Hojjat, R. Iosif, F. Konecny, V. Kuncak, and P. Rummer. In Proc. of FM'12, volume 7436 of LNCS, pages 247-251, 2012. Springer-Verlag. </ref>

<ref name="tacas13">[seplogic.pdf Accelerating Interpolants.] P. Ganty, R. Iosif and F. Konecny. In Proc. of ATVA'12, volume 7561 of LNCS, pages 187-202, 2012. Springer-Verlag. </ref>

<references />