Difference between revisions of "Main Page"

From Numerical Transition Systems
Jump to: navigation, search
Line 6: Line 6:
  
 
* [http://nts.imag.fr/images/b/b5/Ntslib.pdf Language Reference Manual]
 
* [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  
+
* Download [http://nts.imag.fr/images/e/e6/Java-nts.tar.gz 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)
 
* Download [http://nts.imag.fr/images/6/6c/Ocaml-nts.tar.gz OCAML API] (build of 05/02/2013)
 
* [[Benchmarks]]
 
* [[Benchmarks]]

Revision as of 11:11, 5 February 2013

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
Clients
  • Eldarica (a predicate abstraction engine which takes NTS as input)
Projects
  • VERIDYC ANR-09-SEGI-016 (2009-2013)
Events