Difference between revisions of "Main Page"
Radu iosif (Talk | contribs) (→Software) |
Radu iosif (Talk | contribs) (→Software) |
||
| Line 15: | Line 15: | ||
* [[Flata-C]] (C front-end for NTS) | * [[Flata-C]] (C front-end for NTS) | ||
* [[B2NTS]] (converts a subset of Boogie to NTS) | * [[B2NTS]] (converts a subset of Boogie to NTS) | ||
| + | * [[NTS2Horn]] (converts NTS into Horn clauses) | ||
===== Projects ===== | ===== Projects ===== | ||
Revision as of 16:27, 31 January 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 naturals, integers, rationals 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.
Contents
NTS-lib
- Language Reference Manual
- Download Java API
- Download OCAML API
- Benchmarks
Software
- Flata (an NTS verifier)
- Flata-C (C front-end for NTS)
- B2NTS (converts a subset of Boogie to NTS)
- NTS2Horn (converts NTS into Horn clauses)
Projects
- VERIDYC ANR-09-SEGI-016 (2009-2013)
