Difference between revisions of "Flata"

From Numerical Transition Systems
Jump to: navigation, search
Line 1: Line 1:
 
[[File:Octahedron.png|thumb|upright|]]
 
[[File:Octahedron.png|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'''<ref name="fm12">[http://nts.imag.fr/images/c/c2/Fm12.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>
 +
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 control state is reachable
 
* '''reachability analysis''' of non-recursive programs - deciding if an error control state is reachable
Line 14: Line 15:
 
=== 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://nts.imag.fr/images/1/1a/Flata.gz flata.gz]
  
 
Prerequisites:
 
Prerequisites:
Line 33: Line 34:
  
 
* reachability analysis <tt>./flata-reachability.sh benchmarks-reach/VHDL/synlifo.correct.nts</tt>
 
* reachability analysis <tt>./flata-reachability.sh benchmarks-reach/VHDL/synlifo.correct.nts</tt>
* termination analysis  
+
* termination analysis <tt>./flata-termination.sh benchmarks-term/anubhav.correct.nts</tt>
* summary computation <tt>./flata-reachability.sh benchmarks-recur/mccarthy.nts</tt>
+
  
  
Line 41: Line 41:
 
=== Reachability Analysis ===
 
=== Reachability Analysis ===
  
FLATA compu
+
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>. The semi-algorithm is guaranteed to terminate for ''flat integer programs''.
 
+
The core of the analysis is an algorithm from CAV'10.  
+
  
 +
'''Example run'''
 +
* (a correct program) <tt>./flata-reachability.sh benchmarks-reach/VHDL/synlifo.correct.nts</tt>
 +
* (program with a counterexample trace) <tt>./flata-reachability.sh benchmarks-reach/L2CA/listcounter.error.nts</tt>
  
 
=== Termination Analysis ===
 
=== Termination Analysis ===
  
== Verification of Recursive Programs ==
+
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 computing the weakest termination precondition of octagonal relations <ref name="tacas12">[lmcs-draft.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>. The semi-algorithm is guaranteed to terminate for ''flat integer programs''.
  
 +
'''Example run'''
 +
* <tt>./flata-termination.sh benchmarks-term/anubhav.correct.nts</tt>
  
 +
== Verification of Recursive Programs ==
  
== Documentation ==
+
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 a reachability relation between initial and final control states is computed. The semi-algorithm is guaranteed to terminate for ''bounded periodic integer programs''.  
 
+
 
+
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.  
+
  
 +
'''Example run'''
 +
* <tt>./flata-reachability.sh benchmarks-recur/mccarthy.nts</tt>
  
 
== Contributors ==
 
== Contributors ==
Line 77: Line 78:
 
==References==
 
==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="atva12">[http://nts.imag.fr/images/b/b5/Ntslib.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>
 
+
-->
<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 />
 
<references />

Revision as of 16:02, 4 February 2013

Octahedron.png

FLATA<ref name="fm12">"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>

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 control state is reachable
  • 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.gz

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 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 veriify) 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


Verification of Non-recursive Programs

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>. The semi-algorithm is guaranteed to terminate for flat integer programs.

Example run

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

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 computing the weakest termination precondition of octagonal relations <ref name="tacas12">[lmcs-draft.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>. The semi-algorithm is guaranteed to terminate for flat integer programs.

Example run

  • ./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 a reachability relation between initial and final control states is computed. The semi-algorithm is guaranteed to terminate for bounded periodic integer programs.

Example run

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

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.


References

<references />