This year’s challenge will consist of 20 problems, divided into 4 categories. The first three categories 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 problem download page. This years categories are:

• White-Box (basic): this are programs syntactically in the same fashion as for the RERS 2013 challenge. The source code is provided in Java and C.
• White-Box (extended): these are generated in the same fashion as the White-Box (basic) problems (in Java and C), but additionally make use of new language constructs that were not present in the 2013 challenge.

The corresponding collections of properties to be checked against these systems fall into two categories:

1. implicit ones, given by errors/exceptions/assertions. These properties are only implicitly given within the code and should be checked for reachbility. Each individual reachability problem is evaluated and ranked exactly in the same fashion as the explicit properties. There are 100 overall properties for each problem.
2. explicit ones, described verbally and formalized in temporal logic (LTL, the exact syntax is given on this page).

For each problem of the first four categories there are 100 LTL formulae and 100 reachability properties to be answered. For the real world problems the number of inserted errors is not known previously and the contestant with the highest number of discovered faults wins. The submission deadlines can be found on the right. On average there are a least 2 months to analyze the challenge problems, to prepare the results, and to submit the solutions on the submit page. A detailed how-to guide is given on this page.

Evaluation

Achievements

Achievements are not competitive, they are granted for all solutions reaching predefined thresholds.

Competition

There will be two kinds of evaluation or ranking methods used:

1. Quantitative or Numeric: This will be according to the score of correctly put properties. Each correct answer gives one point, but each wrong answer costs two (correct = +1, wrong = -2, and open = 0).
2. Qualitative: This will be according to the employed (combination of) methods. In this category, solutions will be reviewed and ranked by the Challenge Team. Due to the possible variety of methods there may be several winners in this category.

The overall quantitative winner in each category is then determined by the highest ranking.

Rewards

There will be an overall price and price for each kind, as well as a price for the best conceptual contribution in form of a gift certificate for Springer books sponsored by Springer. In addition there will be achievement certificates for every team passing the required threshold. Further information can be found on this page.