Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
cscomp [2011/02/09 19:03] radu.iosif |
cscomp [2011/02/09 19:17] radu.iosif |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Counter Systems Competition (CSComp) ====== | ====== Counter Systems Competition (CSComp) ====== | ||
- | Counter Systems (a.k.a. Counter Automata or Counter Machines) are | + | Counter Systems (a.k.a. Counter Automata or Counter Machines) are simple models of computation involving infinite (or very large) data domains, such as integers, floating-point or real numbers. Despite their apparent simplicity, counter systems 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.). A detailed definition of counter systems of the verification problems we consider can be found here. |
- | simple models of computation involving infinite (or very large) data | + | |
- | domains, such as integers, floating-point or real numbers. Despite | + | |
- | their apparent simplicity, counter systems 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 CSComp is to focus the verification community on a common general format for | + | The aim of CSComp is to focus the verification community on a common general format (cs-lib) for describing counter systems, and to build a open library of benchmarks that will be contributed to by tool developers. |
- | describing counter systems, and to build a open library of benchmarks that will | + | |
- | be contributed to by tool developers. | + | * Rules |
+ | |||
+ | * Download cs-lib | ||
+ | |||
+ | * Sections | ||
+ | |||
+ | * Participants | ||
+ | |||
+ | * Results |