Difference between revisions of "Flata"

From Numerical Transition Systems
Jump to: navigation, search
(Created page with "File:Octahedron.gif '''FLATA''' is a toolset for the manipulation and the analysis of non-deterministic integer programs (also known as counter automata). ...")
 
Line 3: Line 3:
 
'''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:  
 
'''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 anaylysis''' -- deciding if an error state of a non-recursive programs is reachable from an initial state
+
* '''reachability analysis''' of non-recursive programs -- deciding if an error state is reachable from an initial state
  
−
* '''termination analysis''' -- computation of termination preconditions for non-recursive programs
+
* '''termination analysis''' of non-recursive programs -- computation of termination preconditions
  
−
* '''summarization''' for recursive programs --  computation of summaries of recursive programs
+
* computation of '''summaries''' of recursive programs
  
−
The input to the tool is a textual description of a counter automaton (see examples below), essentially a control flow .
 
  
 +
== Running FLATA ==
  
−
== Download ==
+
=== Download ===
−
 
+
  
 
FLATA is a free software under LGPL license. The current distribution of FLATA is available here: [http://www.fit.vutbr.cz/~ikonecny/flata/flata.tgz flata.tgz]
 
FLATA is a free software under LGPL license. The current distribution of FLATA is available here: [http://www.fit.vutbr.cz/~ikonecny/flata/flata.tgz flata.tgz]
−
 
−
A good way to get started using FLATA is to go through one of the examples (a subset of [http://richmodels.epfl.ch/ntscomp/ntslib NTS] benchmarks that FLATA can veriify) linked here:
 
−
[http://www.fit.vutbr.cz/~ikonecny/flata/benchmarks.tgz benchmarks.tgz]
 
−
 
−
 
−
== Installation ==
 
−
 
  
 
Prerequisites:
 
Prerequisites:
Line 32: Line 24:
 
* [http://antlr.org/download/antlr-3.2.jar ANTLR] and [http://www.fit.vutbr.cz/~ikonecny/flata/nts.jar NTS] has to be installed in your JAVA classpath
 
* [http://antlr.org/download/antlr-3.2.jar ANTLR] and [http://www.fit.vutbr.cz/~ikonecny/flata/nts.jar NTS] has to be installed in your JAVA classpath
  
−
Run FLATA as e.g.
 
  
−
{{java -classpath flata.jar:nts.jar:antlr-3.2.jar verimag.flata.Main VHDL/synlifo.correct.nts}}
+
=== Run ===
  
−
See the README file for further information.
+
A good way to get started using FLATA is to go through one of the examples (a subset of [[Main_Page | NTS]] benchmarks that FLATA can veriify) linked here:
 +
[http://www.fit.vutbr.cz/~ikonecny/flata/benchmarks.tgz benchmarks.tgz]
  
 +
The input to the tool is a textual description of a counter automaton (see examples below), essentially a control flow.
  
−
== Documentation ==
+
Run FLATA as e.g.
  
 +
<tt>java -classpath flata.jar:nts.jar:antlr-3.2.jar verimag.flata.Main VHDL/synlifo.correct.nts</tt>
  
−
The following papers are related to the FLATA project:
+
See the README file for further information.
  
−
- M. Bozga, R. Iosif and F. Konecny. [{Fast Acceleration of Ultimately Periodic Relations}->http://www-verimag.imag.fr/TR/TR-2010-3.pdf] VERIMAG TR-2010-3
+
== Verification of Non-recursive Programs ==
  
−
- M. Bozga, C. Girlea and R. Iosif. [{Iterating Octagons}->http://www-verimag.imag.fr/%7Eiosif/papers/tacas09.ps] TACAS 2009
+
=== Reachability Analysis ===
  
−
- M. Bozga, R. Iosif and Y. Lakhnech [{Flat Parametric Counter Automata}->http://www-verimag.imag.fr/%7Eiosif/papers/fundamenta09.ps] Fundamenta Informaticae, Volume 91 (2), 275 - 303, IOS Press (2009)
+
FLATA compu
  
−
A white paper describing the functionalities of the toolset, and including a detailed description of the input syntax and options will be coming soon.  
+
The core of the analysis is an algorithm from CAV'10.  
  
  
−
== Extensions ==
+
=== Termination Analysis ===
  
 +
== Verification of Recursive Programs ==
  
−
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:
 
  
−
- [flata-with-sil jar file->http://www.fit.vutbr.cz/~ikonecny/flata/sil.tgz]
 
−
- [sil-examples.tar.gz->http://www.fit.vutbr.cz/~ikonecny/flata/sil-examples.tgz]
 
  
−
A description of the SIL logic and its applications can be found in the following papers:
+
== Documentation ==
  
−
- P. Habermehl, R. Iosif, T. Vojnar. [{A Logic of Singly Indexed Arrays}->http://www-verimag.imag.fr/%7Eiosif/papers/lpar08.ps] LPAR'08
 
  
−
- M. Bozga, P. Habermehl, R. Iosif, F. Konecny, T. Vojnar. [{Automatic Verification of Integer Array Programs}->http://www-verimag.imag.fr/%7Eiosif/papers/cav09.ps] CAV'09
+
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.  
  
  
Line 81: Line 74:
 
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.
 
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==
 +
 +
{{reflist}}
  
 
==References==
 
==References==

Revision as of 12:31, 4 February 2013

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.


Termination Analysis

Verification of Recursive Programs

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


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

Template:Reflist

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 />

Retrieved from "http://nts.imag.fr/index.php?title=Flata&oldid=60"