Numerical Transition Systems - User contributions [en]

Flata

2013-09-04T16:51:06Z

Konecny: /* Decision Procedure for the SAT problem of the Logic SIL */

'''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. Garnier, 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 - 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 here: [http://nts.imag.fr/images/3/3a/Flata.tar.gz flata.tar.gz]

Prerequisites:

* [http://www.java.com/en/ JAVA] version 1.6.0 or later

* [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)



== 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 [[Main_Page | NTS]] benchmarks that FLATA can verify) contained in the distribution and run FLATA as e.g.:

* 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 ==

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)

== 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. ([http://arxiv.org/pdf/1302.2762v1 Extended journal submission.]) </ref>.

'''Example'''
* <tt>./flata-termination.sh benchmarks-term/anubhav.correct.nts</tt>

== 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">[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>

== Decision Procedure for the SAT problem of the Logic SIL ==

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.


'''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 ==

* [http://www-verimag.imag.fr/%7Ebozga Marius Bozga] (VERIMAG, Grenoble, France)
* [http://www-verimag.imag.fr/%7Eiosif Radu Iosif] (VERIMAG, Grenoble, France)
* [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)

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

Flata

2013-09-04T16:48:42Z

Konecny: /* Decision Procedure for the SAT problem of the Logic SIL */

'''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. Garnier, 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 - 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 here: [http://nts.imag.fr/images/3/3a/Flata.tar.gz flata.tar.gz]

Prerequisites:

* [http://www.java.com/en/ JAVA] version 1.6.0 or later

* [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)



== 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 [[Main_Page | NTS]] benchmarks that FLATA can verify) contained in the distribution and run FLATA as e.g.:

* 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 ==

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)

== 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. ([http://arxiv.org/pdf/1302.2762v1 Extended journal submission.]) </ref>.

'''Example'''
* <tt>./flata-termination.sh benchmarks-term/anubhav.correct.nts</tt>

== 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">[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>

== Decision Procedure for the SAT problem of the Logic SIL ==

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

'''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 ==

* [http://www-verimag.imag.fr/%7Ebozga Marius Bozga] (VERIMAG, Grenoble, France)
* [http://www-verimag.imag.fr/%7Eiosif Radu Iosif] (VERIMAG, Grenoble, France)
* [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)

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

File:Flata.tar.gz

2013-09-04T16:02:09Z

Konecny: Konecny uploaded a new version of "File:Flata.tar.gz"

File:Flata.tar.gz

2013-09-04T16:00:48Z

Konecny: Konecny uploaded a new version of "File:Flata.tar.gz"

File:Flata.tar.gz

2013-09-03T13:16:07Z

Konecny: Konecny uploaded a new version of "File:Flata.tar.gz"

Flata

2013-09-03T12:49:37Z

Konecny:

'''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. Garnier, 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 - 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 here: [http://nts.imag.fr/images/3/3a/Flata.tar.gz flata.tar.gz]

Prerequisites:

* [http://www.java.com/en/ JAVA] version 1.6.0 or later

* [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)



== 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 [[Main_Page | NTS]] benchmarks that FLATA can verify) contained in the distribution and run FLATA as e.g.:

* 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 ==

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)

== 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. ([http://arxiv.org/pdf/1302.2762v1 Extended journal submission.]) </ref>.

'''Example'''
* <tt>./flata-termination.sh benchmarks-term/anubhav.correct.nts</tt>

== 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">[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>

== Decision Procedure for the SAT problem of the Logic SIL ==

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 which is known to be decidable<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>.

'''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 ==

* [http://www-verimag.imag.fr/%7Ebozga Marius Bozga] (VERIMAG, Grenoble, France)
* [http://www-verimag.imag.fr/%7Eiosif Radu Iosif] (VERIMAG, Grenoble, France)
* [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)

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

File:Ntslib.pdf

2013-06-24T15:47:10Z

Konecny: Konecny uploaded a new version of "File:Ntslib.pdf"

File:Sil-examples.tar.gz

2013-04-02T16:15:34Z

Konecny:

File:Sil.tar.gz

2013-04-02T16:15:25Z

Konecny:

File:Flata.tar.gz

2013-03-15T11:33:30Z

Konecny: Konecny uploaded a new version of "File:Flata.tar.gz"

File:Flata.tar.gz

2013-03-15T11:17:30Z

Konecny: Konecny uploaded a new version of "File:Flata.tar.gz"

Flata

2013-03-04T17:57:13Z

Konecny:

'''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. Garnier, 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 - 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 here: [http://nts.imag.fr/images/3/3a/Flata.tar.gz flata.tar.gz]

Prerequisites:

* [http://www.java.com/en/ JAVA] version 1.6.0 or later

* [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)



== 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 [[Main_Page | NTS]] benchmarks that FLATA can verify) contained in the distribution and run FLATA as e.g.:

* 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 ==

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)

== 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. ([http://arxiv.org/pdf/1302.2762v1 Extended journal submission.]) </ref>.

'''Example'''
* <tt>./flata-termination.sh benchmarks-term/anubhav.correct.nts</tt>

== 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">[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>

== Contributors ==

* [http://www-verimag.imag.fr/%7Ebozga Marius Bozga] (VERIMAG, Grenoble, France)
* [http://www-verimag.imag.fr/%7Eiosif Radu Iosif] (VERIMAG, Grenoble, France)
* [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)

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

Flata

2013-02-13T08:10:27Z

Konecny:

'''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. Garnier, 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 - 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 here: [http://nts.imag.fr/images/3/3a/Flata.tar.gz flata.tar.gz]

Prerequisites:

* [http://www.java.com/en/ JAVA] version 1.6.0 or later

* [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)



== 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 [[Main_Page | NTS]] benchmarks that FLATA can verify) contained in the distribution and run FLATA as e.g.:

* 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 ==

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)

== 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. ([http://arxiv.org/pdf/1302.2762v1 Extended journal submission.]) </ref>.

'''Example'''
* <tt>./flata-termination.sh benchmarks-term/anubhav.correct.nts</tt>

== 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">[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>

== Contributors ==

* [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/~konecny/ Filip Konecny] (EPFL, Lausanne, Switzerland)
* [http://www.fit.vutbr.cz/~vojnar/ 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.

==References==



<references />

Flata

2013-02-05T10:25:23Z

Konecny:

'''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. Garnier, 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 - 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 here: [http://nts.imag.fr/images/3/3a/Flata.tar.gz flata.tar.gz]

Prerequisites:

* [http://www.java.com/en/ JAVA] version 1.6.0 or later

* [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)



== 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 [[Main_Page | NTS]] benchmarks that FLATA can verify) contained in the distribution and run FLATA as e.g.:

* 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 ==

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)

== 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. ([http://arxiv.org/pdf/1210.42.pdf Extended journal submission.]) </ref>. The semi-algorithm is guaranteed to terminate for ''flat integer programs''.

'''Example'''
* <tt>./flata-termination.sh benchmarks-term/anubhav.correct.nts</tt>

== 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">[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>

== Contributors ==

* [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/~konecny/ Filip Konecny] (EPFL, Lausanne, Switzerland)
* [http://www.fit.vutbr.cz/~vojnar/ 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.

==References==



<references />

Flata

2013-02-04T15:22:22Z

Konecny:

[[File:Octahedron.png|thumb|upright|]]

'''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 - checking 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: [http://nts.imag.fr/images/3/3a/Flata.tar.gz flata.tar.gz]

Prerequisites:

* [http://www.java.com/en/ JAVA] version 1.6.0 or later

* [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)



=== 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 [[Main_Page | NTS]] benchmarks that FLATA can veriify) contained in the distribution and run FLATA as e.g.:

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

== 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">[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''.

'''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 ===

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/1210.42.pdf Extended journal submission.]) </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 ==

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

'''Example run'''
* <tt>./flata-reachability.sh benchmarks-recur/mccarthy.nts</tt>

== Contributors ==

* [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/~konecny/ Filip Konecny] (VERIMAG and Brno University of Technology)
* [http://www.fit.vutbr.cz/~vojnar/ 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.

==References==



<references />

Flata

2013-02-04T15:12:20Z

Konecny:

[[File:Octahedron.png|thumb|upright|]]

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

* '''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: [http://nts.imag.fr/images/3/3a/Flata.tar.gz flata.tar.gz]

Prerequisites:

* [http://www.java.com/en/ JAVA] version 1.6.0 or later

* [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)



=== 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 [[Main_Page | NTS]] benchmarks that FLATA can veriify) contained in the distribution and run FLATA as e.g.:

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

== 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">[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''.

'''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 ===

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

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''.

'''Example run'''
* <tt>./flata-reachability.sh benchmarks-recur/mccarthy.nts</tt>

== Contributors ==

* [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/~konecny/ Filip Konecny] (VERIMAG and Brno University of Technology)
* [http://www.fit.vutbr.cz/~vojnar/ 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.

==References==



<references />

File:Flata.tar.gz

2013-02-04T15:10:20Z

Konecny:

File:Octahedron.png

2013-02-04T15:06:12Z

Konecny:

Flata

2013-02-04T15:02:57Z

Konecny:

[[File:Octahedron.png|thumb|upright|]]

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

* '''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: [http://nts.imag.fr/images/1/1a/Flata.gz flata.gz]

Prerequisites:

* [http://www.java.com/en/ JAVA] version 1.6.0 or later

* [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)



=== 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 [[Main_Page | NTS]] benchmarks that FLATA can veriify) contained in the distribution and run FLATA as e.g.:

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

== 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">[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''.

'''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 ===

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

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''.

'''Example run'''
* <tt>./flata-reachability.sh benchmarks-recur/mccarthy.nts</tt>

== Contributors ==

* [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/~konecny/ Filip Konecny] (VERIMAG and Brno University of Technology)
* [http://www.fit.vutbr.cz/~vojnar/ 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.

==References==



<references />

File:Fm12.pdf

2013-02-04T15:00:58Z

Konecny:

File:Cav10.pdf

2013-02-04T14:57:39Z

Konecny:

File:Flata.gz

2013-02-04T14:51:58Z

Konecny:

Flata

2013-02-04T13:29:22Z

Konecny:

[[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:

* '''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: [http://www.fit.vutbr.cz/~ikonecny/flata/flata.tgz flata.tgz]

Prerequisites:

* [http://www.java.com/en/ JAVA] version 1.6.0 or later

* [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)



=== 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 [[Main_Page | NTS]] benchmarks that FLATA can veriify) contained in the distribution and run FLATA as e.g.:

* reachability analysis <tt>./flata-reachability.sh benchmarks-reach/VHDL/synlifo.correct.nts</tt>
* termination analysis
* summary computation <tt>./flata-reachability.sh benchmarks-recur/mccarthy.nts</tt>

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

* [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/~konecny/ Filip Konecny] (VERIMAG and Brno University of Technology)
* [http://www.fit.vutbr.cz/~vojnar/ 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.

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

File:Octaheron.png

2013-02-04T12:30:17Z

Konecny:

Flata

2013-02-04T11:31:01Z

Konecny:

[[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:

* '''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: [http://www.fit.vutbr.cz/~ikonecny/flata/flata.tgz flata.tgz]

Prerequisites:

* [http://www.java.com/en/ JAVA] version 1.6.0 or later

* [http://yices.csl.sri.com/download.shtml YICES] has to be installed in your executable path

* [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 ===

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.

Run FLATA as e.g.

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

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

* [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/~konecny/ Filip Konecny] (VERIMAG and Brno University of Technology)
* [http://www.fit.vutbr.cz/~vojnar/ 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==

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

Flata

2013-02-04T10:53:52Z

Konecny: Created page with "upright| '''FLATA''' is a toolset for the manipulation and the analysis of non-deterministic integer programs (also known as counter automata). ..."

[[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:

* '''reachability anaylysis''' -- deciding if an error state of a non-recursive programs is reachable from an initial state

* '''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 .

== 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]

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:

* [http://www.java.com/en/ JAVA] version 1.6.0 or later

* [http://yices.csl.sri.com/download.shtml YICES] has to be installed in your executable path

* [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}}

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}->http://www-verimag.imag.fr/TR/TR-2010-3.pdf] VERIMAG TR-2010-3

- M. Bozga, C. Girlea and R. Iosif. [{Iterating Octagons}->http://www-verimag.imag.fr/%7Eiosif/papers/tacas09.ps] TACAS 2009

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

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:

- [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:

- 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

== Contributors ==

* [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/~konecny/ Filip Konecny] (VERIMAG and Brno University of Technology)
* [http://www.fit.vutbr.cz/~vojnar/ 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.

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

File:Octahedron.gif

2013-02-04T10:33:52Z

Konecny:

Main Page

2013-01-31T16:20:24Z

Konecny: Undo revision 40 by Konecny (talk)

'''Numerical Transition Systems Repository'''

Numerical Transition Systems (a.k.a. Counter Systems, Counter Automata or Counter Machines) are simple models of computation involving infinite (or very large) data domains, such as integers or real numbers. Despite their apparent simplicity, NTS can, in theory, model any real-life computer system, ranging from hardware circuits to programs. As a consequence, an important number of tools have emerged, addressing verification problems, such as reachability or termination, and deploying various techniques (widening, predicate abstraction, acceleration, etc.). The aim of NTS is to focus the verification community on a common general format (NTS-lib) for describing NTS, and to build a open library of benchmarks that will be contributed to by tool developers.

===== NTS-lib =====

* [[Language Reference Manual]][[Media::Ntslib.pdf]]
* Download [[Media:Java-nts.tar.gz]]
* Download [[OCAML API]]
* [[Benchmarks]]

===== Software =====

* [[Flata]] (an NTS verifier)
* [[Flata-C]] (C front-end for NTS)
* [[boogie2nts]] (converts a subset of Boogie to NTS)
* [[nts2horn]] (converts NTS into Horn clauses)

===== Projects =====

* [https://sites.google.com/site/veridyc VERIDYC] ANR-09-SEGI-016 (2009-2013)

===== Events =====

* [[AVM 2014]]

Main Page

2013-01-31T16:19:32Z

Konecny: /* NTS-lib */

'''Numerical Transition Systems Repository'''

Numerical Transition Systems (a.k.a. Counter Systems, Counter Automata or Counter Machines) are simple models of computation involving infinite (or very large) data domains, such as integers or real numbers. Despite their apparent simplicity, NTS can, in theory, model any real-life computer system, ranging from hardware circuits to programs. As a consequence, an important number of tools have emerged, addressing verification problems, such as reachability or termination, and deploying various techniques (widening, predicate abstraction, acceleration, etc.). The aim of NTS is to focus the verification community on a common general format (NTS-lib) for describing NTS, and to build a open library of benchmarks that will be contributed to by tool developers.

===== NTS-lib =====

* [[Language Reference Manual]][[Media::Ntslib.pdf]]
* Download [[Java API:Java-nts.tar.gz]]
* Download [[OCAML API]]
* [[Benchmarks]]

===== Software =====

* [[Flata]] (an NTS verifier)
* [[Flata-C]] (C front-end for NTS)
* [[boogie2nts]] (converts a subset of Boogie to NTS)
* [[nts2horn]] (converts NTS into Horn clauses)

===== Projects =====

* [https://sites.google.com/site/veridyc VERIDYC] ANR-09-SEGI-016 (2009-2013)

===== Events =====

* [[AVM 2014]]

Main Page

2013-01-31T16:19:08Z

Konecny: /* NTS-lib */

Main Page

2013-01-31T16:18:28Z

Konecny: /* NTS-lib */

'''Numerical Transition Systems Repository'''

Numerical Transition Systems (a.k.a. Counter Systems, Counter Automata or Counter Machines) are simple models of computation involving infinite (or very large) data domains, such as integers or real numbers. Despite their apparent simplicity, NTS can, in theory, model any real-life computer system, ranging from hardware circuits to programs. As a consequence, an important number of tools have emerged, addressing verification problems, such as reachability or termination, and deploying various techniques (widening, predicate abstraction, acceleration, etc.). The aim of NTS is to focus the verification community on a common general format (NTS-lib) for describing NTS, and to build a open library of benchmarks that will be contributed to by tool developers.

===== NTS-lib =====

* [[Language Reference Manual:Ntslib.pdf]]
* Download [[Java-nts.tar.gz]]
* Download [[OCAML API]]
* [[Benchmarks]]

===== Software =====

* [[Flata]] (an NTS verifier)
* [[Flata-C]] (C front-end for NTS)
* [[boogie2nts]] (converts a subset of Boogie to NTS)
* [[nts2horn]] (converts NTS into Horn clauses)

===== Projects =====

* [https://sites.google.com/site/veridyc VERIDYC] ANR-09-SEGI-016 (2009-2013)

===== Events =====

* [[AVM 2014]]

Main Page

2013-01-31T16:17:44Z

Konecny: /* NTS-lib */

'''Numerical Transition Systems Repository'''

Numerical Transition Systems (a.k.a. Counter Systems, Counter Automata or Counter Machines) are simple models of computation involving infinite (or very large) data domains, such as integers or real numbers. Despite their apparent simplicity, NTS can, in theory, model any real-life computer system, ranging from hardware circuits to programs. As a consequence, an important number of tools have emerged, addressing verification problems, such as reachability or termination, and deploying various techniques (widening, predicate abstraction, acceleration, etc.). The aim of NTS is to focus the verification community on a common general format (NTS-lib) for describing NTS, and to build a open library of benchmarks that will be contributed to by tool developers.

===== NTS-lib =====

* [[Language Reference Manual:Ntslib.pdf]]
* Download [[Java API:Java-nts.tar.gz]]
* Download [[OCAML API]]
* [[Benchmarks]]

===== Software =====

* [[Flata]] (an NTS verifier)
* [[Flata-C]] (C front-end for NTS)
* [[boogie2nts]] (converts a subset of Boogie to NTS)
* [[nts2horn]] (converts NTS into Horn clauses)

===== Projects =====

* [https://sites.google.com/site/veridyc VERIDYC] ANR-09-SEGI-016 (2009-2013)

===== Events =====

* [[AVM 2014]]

File:Java-nts.tar.gz

2013-01-31T16:15:26Z

Konecny:

File:Ntslib.pdf

2013-01-31T15:52:21Z

Konecny: