Main Page - Revision history

Radu iosif at 15:52, 6 May 2014

2014-05-06T15:52:24Z

Radu iosif at 13:47, 14 June 2013

2013-06-14T13:47:55Z

Radu iosif at 13:44, 14 June 2013

2013-06-14T13:44:46Z

Radu iosif at 13:44, 14 June 2013

2013-06-14T13:44:28Z

Radu iosif at 13:43, 14 June 2013

2013-06-14T13:43:53Z

Radu iosif at 13:43, 14 June 2013

2013-06-14T13:43:14Z

Radu iosif at 13:42, 14 June 2013

2013-06-14T13:42:42Z

Radu iosif at 13:42, 14 June 2013

2013-06-14T13:42:24Z

Radu iosif at 13:22, 14 June 2013

2013-06-14T13:22:50Z

Radu iosif at 13:22, 14 June 2013

2013-06-14T13:22:36Z

@@ Line 6: / Line 6: @@
 * [http://nts.imag.fr/images/b/b5/Ntslib.pdf Language Reference Manual]
-* Download [http://nts.imag.fr/images/e/e6/Java-nts.tar.gz Java API] (build of 31/01/2013)
+* Download the [https://github.com/filipkonecny/nts Java API] (build of 31/01/2013)
-* Download [http://nts.imag.fr/images/6/6c/Ocaml-nts.tar.gz OCAML API] (build of 05/02/2013)
 * [[Benchmarks]]

@@ Line 13: / Line 13: @@
 * [[Flata]] (an NTS verifier)
-* [[https://github.com/fgarnier/flatac Flata-C]] (C front-end for NTS)
+* [https://github.com/fgarnier/flatac Flata-C] (C front-end for NTS)
 * [https://github.com/pierreganty/c2s c2s] (converts a subset of Boogie to NTS, part of the c2s tool)

@@ Line 3: / Line 3: @@
 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 ===
+==== NTS-lib ====
 * [http://nts.imag.fr/images/b/b5/Ntslib.pdf Language Reference Manual]

@@ Line 3: / Line 3: @@
 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 ===
+==== NTS-lib ===
 * [http://nts.imag.fr/images/b/b5/Ntslib.pdf Language Reference Manual]
@@ Line 10: / Line 10: @@
 * [[Benchmarks]]
-===== Software =====
+==== Software ====
 * [[Flata]] (an NTS verifier)
@@ Line 16: / Line 16: @@
 * [https://github.com/pierreganty/c2s c2s] (converts a subset of Boogie to NTS, part of the c2s tool)
-===== Clients =====
+==== Clients ====
 * [http://lara.epfl.ch/w/eldarica Eldarica] (a predicate abstraction engine which takes NTS as input, and also converts NTS into Prolog Horn Clause format)
-===== Projects =====
+==== Projects ====
 * [https://sites.google.com/site/veridyc VERIDYC] ANR-09-SEGI-016 (2009-2013)
-===== Events =====
+==== Events ====
 * [[AVM 2014]] Alpine Verification Meeting 2014, Frejus, France

@@ Line 3: / Line 3: @@
 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 =====
+=== NTS-lib ===
 * [http://nts.imag.fr/images/b/b5/Ntslib.pdf Language Reference Manual]

← Older revision		Revision as of 13:43, 14 June 2013
Line 1:		Line 1:
−	'Numerical Transition Systems Repository'	+	== 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.		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.

← Older revision		Revision as of 13:42, 14 June 2013
Line 1:		Line 1:
−	''Numerical Transition Systems Repository''	+	'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.		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.

@@ Line 18: / Line 18: @@
 ===== Clients =====
-* [http://lara.epfl.ch/w/eldarica Eldarica] (a predicate abstraction engine which takes NTS as input)
+* [http://lara.epfl.ch/w/eldarica Eldarica] (a predicate abstraction engine which takes NTS as input, and also converts NTS into Horn Clause format)
 ===== Projects =====