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). ...")
 
 
(24 intermediate revisions by 2 users not shown)
Line 1: Line 1:
[[File:Octahedron.gif|thumb|upright|]]
 
 
 
'''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 - checking if an error control state is reachable
 
+
* '''termination analysis''' -- computation of termination preconditions for non-recursive programs
+
 
+
* '''summarization''' for 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 .
+
* '''termination analysis''' of non-recursive programs - computation of termination preconditions
  
 +
* computation of '''summaries''' of recursive programs
  
 
== Download ==
 
== Download ==
  
 
+
FLATA is a free software under LGPL license. The current distribution of FLATA is available as an [http://nts.imag.fr/images/3/3a/Flata.tar.gz archive] or on this [https://github.com/filipkonecny/flata git repository]
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 30: Line 17:
 
* [http://yices.csl.sri.com/download.shtml YICES] has to be installed in your executable path
 
* [http://yices.csl.sri.com/download.shtml YICES] has to be installed in your executable path
  
 +
* [http://glpk-java.sourceforge.net/ GLPK Java] has to be installed in LD_LIBRARY_PATH (required for termination analysis only)
 +
 +
<!--
 
* [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.
+
== Run ==
  
{{java -classpath flata.jar:nts.jar:antlr-3.2.jar verimag.flata.Main VHDL/synlifo.correct.nts}}
+
The input to the tool is a textual description of a counter automaton, essentially a control flow graph with edges labeled with arithmetic relations. A good way to get started using FLATA is to go through some of the examples (a subset of [[Main_Page | NTS]] benchmarks that FLATA can verify) contained in the distribution and run FLATA as e.g.:
  
See the README file for further information.
+
* reachability analysis <tt>./flata-reachability.sh benchmarks-reach/VHDL/synlifo.correct.nts</tt>
 +
* termination analysis <tt>./flata-termination.sh benchmarks-term/anubhav.correct.nts</tt>
  
 +
== Reachability Analysis ==
  
== Documentation ==
+
The reachability analysis semi-algorithm implemented in FLATA is based on computatation of procedure summaries. The core of the method is an algorithm for computing transitive closures of octagonal relations <ref name="cav10">[http://nts.imag.fr/images/d/d5/Cav10.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="cav10-TR">[http://www-verimag.imag.fr/TR/TR-2012-10.pdf "Relational Analysis of Integer Programs"] M. Bozga, R. Iosif, and F. Konecny. VERIMAG technical report, TR-2012-10, 2012. </ref>.
  
 +
'''Examples'''
 +
* <tt>./flata-reachability.sh benchmarks-reach/VHDL/synlifo.correct.nts</tt> (a correct program)
 +
* <tt>./flata-reachability.sh benchmarks-reach/L2CA/listcounter.error.nts</tt> (program with a counterexample trace)
  
The following papers are related to the FLATA project:
+
== Termination Analysis ==
  
- 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
+
The semi-algorithm implemented in FLATA first attempts to compute a transition invariant as a disjunction of octagonal relations (by adapting the procedure summary algorithm) and then computes a termination precondition by applying an algorithm that computes the weakest termination precondition of octagonal relations <ref name="tacas12"> 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. ([http://arxiv.org/pdf/1302.2762v1 Extended journal submission.]) </ref>.
  
- M. Bozga, C. Girlea and R. Iosif. [{Iterating Octagons}->http://www-verimag.imag.fr/%7Eiosif/papers/tacas09.ps] TACAS 2009
+
'''Example'''
 +
* <tt>./flata-termination.sh benchmarks-term/anubhav.correct.nts</tt>
  
- 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)
+
== Verification of Recursive Programs ==
  
A white paper describing the functionalities of the toolset, and including a detailed description of the input syntax and options will be coming soon.  
+
Given a recursive program, FLATA attempts to compute its summary by computing increasingly precise underapproximations of the program <ref name="tacas13">[http://arxiv.org/pdf/1210.4289.pdf "Underapproximation of Procedure Summaries for Integer Programs."] P. Ganty, R. Iosif and F. Konecny.  In Proc. of TACAS'13. To appear. </ref>. Note that error control states are ignored and that a reachability relation between initial and final control states is computed.  
  
 +
'''Example'''
 +
* <tt>./flata-reachability.sh benchmarks-recur/mccarthy.nts</tt>
  
== Extensions ==
 
  
 +
== Decision Procedure for the SAT problem of the Logic SIL ==
  
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 decides the satisfiability problem of the SIL logic<ref name="lpar-08">[http://nts.imag.fr/images/d/d3/Lpar08.pdf "A Logic of Singly Indexed Arrays"] P. Habermehl, R. Iosif, T. Vojnar. In Proc. of LPAR'08, volume 5330 of LNCS, pages 558-573, 2008. Springer-Verlag. </ref> by reduction to the reachability problem of flat counter automata.
 
+
<!--
- [flata-with-sil jar file->http://www.fit.vutbr.cz/~ikonecny/flata/sil.tgz]
+
<ref name="comon-jurski"> "Multiple counters automata, safety analysis and presburger arithmetic". In Proc. of CAV, volume 1427 of LNCS, pages 268–279, Berlin, Heidelberg, 1998. Springer Verlag.</ref>
- [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:
+
 
+
- 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
+
  
 +
'''Examples'''
 +
* <tt>./flata-sil.sh benchmarks-sil/rotation_vc.nts</tt> (valid formula)
 +
* <tt>./flata-sil.sh benchmarks-sil/rotation_vc-f.nts</tt> (falsifiable formula)
  
 
== Contributors ==
 
== Contributors ==
Line 73: Line 69:
 
* [http://www-verimag.imag.fr/%7Ebozga Marius Bozga] (VERIMAG, Grenoble, France)
 
* [http://www-verimag.imag.fr/%7Ebozga Marius Bozga] (VERIMAG, Grenoble, France)
 
* [http://www-verimag.imag.fr/%7Eiosif Radu Iosif] (VERIMAG, Grenoble, France)
 
* [http://www-verimag.imag.fr/%7Eiosif Radu Iosif] (VERIMAG, Grenoble, France)
* [http://www-verimag.imag.fr/~konecny/ Filip Konecny] (VERIMAG and Brno University of Technology)
+
* [http://people.epfl.ch/filip.konecny Filip Konecny] (EPFL, Lausanne, Switzerland)
 
* [http://www.fit.vutbr.cz/~vojnar/ Tomas Vojnar] (Brno University of Technology, Czech Republic)
 
* [http://www.fit.vutbr.cz/~vojnar/ Tomas Vojnar] (Brno University of Technology, Czech Republic)
  
  
 
== Acknowledgements ==
 
== 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.
 
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.
 
 
==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 />
 

Latest revision as of 15:06, 29 December 2016

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 - checking if an error control state is reachable
  • termination analysis of non-recursive programs - computation of termination preconditions
  • computation of summaries of recursive programs

Download

FLATA is a free software under LGPL license. The current distribution of FLATA is available as an archive or on this git repository

Prerequisites:

  • JAVA version 1.6.0 or later
  • YICES has to be installed in your executable path
  • GLPK Java has to be installed in LD_LIBRARY_PATH (required for termination analysis only)


Run

The input to the tool is a textual description of a counter automaton, essentially a control flow graph with edges labeled with arithmetic relations. A good way to get started using FLATA is to go through some of the examples (a subset of NTS benchmarks that FLATA can verify) contained in the distribution and run FLATA as e.g.:

  • reachability analysis ./flata-reachability.sh benchmarks-reach/VHDL/synlifo.correct.nts
  • termination analysis ./flata-termination.sh benchmarks-term/anubhav.correct.nts

Reachability Analysis

The reachability analysis semi-algorithm implemented in FLATA is based on computatation of procedure summaries. The core of the method is an algorithm for computing transitive closures of octagonal relations <ref name="cav10">"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="cav10-TR">"Relational Analysis of Integer Programs" M. Bozga, R. Iosif, and F. Konecny. VERIMAG technical report, TR-2012-10, 2012. </ref>.

Examples

  • ./flata-reachability.sh benchmarks-reach/VHDL/synlifo.correct.nts (a correct program)
  • ./flata-reachability.sh benchmarks-reach/L2CA/listcounter.error.nts (program with a counterexample trace)

Termination Analysis

The semi-algorithm implemented in FLATA first attempts to compute a transition invariant as a disjunction of octagonal relations (by adapting the procedure summary algorithm) and then computes a termination precondition by applying an algorithm that computes the weakest termination precondition of octagonal relations <ref name="tacas12"> 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. (Extended journal submission.) </ref>.

Example

  • ./flata-termination.sh benchmarks-term/anubhav.correct.nts

Verification of Recursive Programs

Given a recursive program, FLATA attempts to compute its summary by computing increasingly precise underapproximations of the program <ref name="tacas13">"Underapproximation of Procedure Summaries for Integer Programs." P. Ganty, R. Iosif and F. Konecny. In Proc. of TACAS'13. To appear. </ref>. Note that error control states are ignored and that a reachability relation between initial and final control states is computed.

Example

  • ./flata-reachability.sh benchmarks-recur/mccarthy.nts


Decision Procedure for the SAT problem of the Logic SIL

FLATA decides the satisfiability problem of the SIL logic<ref name="lpar-08">"A Logic of Singly Indexed Arrays" P. Habermehl, R. Iosif, T. Vojnar. In Proc. of LPAR'08, volume 5330 of LNCS, pages 558-573, 2008. Springer-Verlag. </ref> by reduction to the reachability problem of flat counter automata.

Examples

  • ./flata-sil.sh benchmarks-sil/rotation_vc.nts (valid formula)
  • ./flata-sil.sh benchmarks-sil/rotation_vc-f.nts (falsifiable formula)

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.