This year’s challenge will consist of both sequential and parallel verification benchmarks. 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 "true" and "false" 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

This year's parallel track is:

• Parallel LTL: 20 LTL properties are provided per benchmark system that have to be verified or falsified by participants. See the parallel problem description for details.

---

Sequential Problems

This year's sequential tracks are:

• Sequential LTL: 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).
• Sequential Reachability: 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 C99 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 additionally 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 this page. It provides information on how the code can be modified to be run and how the function call can be interpreted.