This year’s challenge will consist of 28 problems, divided into 2 tracks. 18 sequential problems that are devided into 2 categories and 10 parallel problems. The problems will range from structurally simple and small to structurally complex and huge. More detailed information about the exact generation process and syntax of the problems can be found on the sequential problem description page and the parallel problem description page. Please note that the syntax of the LTL properties is not equal so read the descriptions carefully.

For successfully answering of questions there will be rewards and achievements for which further information can be found on this page. It is not required to submit the code that produced the challenge results. Only the "yes" and "no" answers in the submitted solutions are considered for the ranking and achievements. For winning an evaluation-based award it is however required to describe the approach for computing the solutions. The submit page gives detailed information about how the solutions have to be submitted. There are no constraints on the application of methods, so participants can modify the source code in any way imaginable. In particular participants are not constrained to their own tools.

Parallel Problems

For each parallel problem there are 3 files provided. A Promela file containing executable promela code, a DOT file containing a visualization of the transition system and the property file containing the 20 LTL properties that have to be analyzed. A detailed description of how the parallel systems are constructed and the property semantics and syntax can be found on the this page.

Sequential Problems

This years sequential categories are:

• LTL Problems: for these programs a constraints file is provided that contains properties to be checked. The properties are described verbally and formalized in temporal logic (LTL, the exact syntax is given on this page).
• Reachability Problems: for these programs the reachability of an external function call has to be verified. Therefore the reachability question is given implicitly given within the source code. LTL formula are not provided. .

The source code is provided in Java and C for both problem types. For each problem 100 properties have to be verified. For the LTL problems 100 LTL formulae and for the reachability problems 100 reachability properties can be answered.

LTL Problems

For each problem there are 3 files provided. The C source code file (ProblemX.c), the Java source code file (ProblemX.java) and a constraints file containing 100 LTL properties. A detailed description of the code layout can be found on the this page.

Reachability Problems

The reachability problems are generated in the same fashion as the LTL problems, but addionally contain function calls to the external __VERIFIER_error(int) function that is not defined in the source code. The source can therefore not be complied without modifications. A detailed description of the code layout can be found on the this page. It gives information on how the code can be modified to be run and how the function call can be interpreted.