Difference between revisions of "Main Page"

From Numerical Transition Systems
Jump to: navigation, search
(NTS-lib)
 
(23 intermediate revisions by 2 users not shown)
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.
  
===== NTS-lib =====
+
==== NTS-lib ====
  
* [Media::Ntslib.pdf Language Reference Manual]
+
* [http://nts.imag.fr/images/b/b5/Ntslib.pdf Language Reference Manual]
* Download [[Media:Java-nts.tar.gz]]
+
* Download the [https://github.com/filipkonecny/nts Java API] (build of 31/01/2013)
* Download [[OCAML API]]
+
 
* [[Benchmarks]]
 
* [[Benchmarks]]
  
===== Software =====
+
==== Software ====
  
 
* [[Flata]] (an NTS verifier)
 
* [[Flata]] (an NTS verifier)
* [[Flata-C]] (C front-end for NTS)
+
* [https://github.com/fgarnier/flatac Flata-C] (C front-end for NTS)
* [[boogie2nts]] (converts a subset of Boogie to NTS)
+
* [https://github.com/pierreganty/c2s c2s] (converts a subset of Boogie to NTS, part of the c2s tool)
* [[nts2horn]] (converts NTS into Horn clauses)
+
  
===== Projects =====
+
==== 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 ====
  
 
* [https://sites.google.com/site/veridyc VERIDYC] ANR-09-SEGI-016 (2009-2013)
 
* [https://sites.google.com/site/veridyc VERIDYC] ANR-09-SEGI-016 (2009-2013)
  
===== Events =====
+
==== Events ====
+
 
* [[AVM 2014]]
+
* [[AVM 2014]] Alpine Verification Meeting 2014, Frejus, France

Latest revision as of 16:52, 6 May 2014

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

Software

  • Flata (an NTS verifier)
  • Flata-C (C front-end for NTS)
  • c2s (converts a subset of Boogie to NTS, part of the c2s tool)

Clients

  • Eldarica (a predicate abstraction engine which takes NTS as input, and also converts NTS into Prolog Horn Clause format)

Projects

  • VERIDYC ANR-09-SEGI-016 (2009-2013)

Events

  • AVM 2014 Alpine Verification Meeting 2014, Frejus, France