Important Dates:

For Participants



Challenge Setup and Rules

The challenge problems are of three kinds which correspond to the prize categories, and whose corresponding problems are organized in four dimensions:

  • language features: plain, arithmetic, arrays,
  • system size: small, medium, large,
  • behavioral complexity: small, medium, large,
  • properties: reachability, safety properties, full LTL.

This means that for each kind 27 reactive systems must be considered which range from plain, structurally simple and small systems to structurally complex and huge systems comprising arithmetic and arrays. All these systems must be checked for 100 properties, which 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.
  2. explicit ones, described verbally and formalized in temporal logic.


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.


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 certificates for the first three in each category, and achievement certificates for every team passing the required threshold.

The teams with the best solutions in their categories will be invited for a STTT Special Section summarizing the results of the challenge, and, in particular, presenting the most advanced solutions.