RERS has a 3-dimensional reward structure:

1. achievement certificates in gold, silver and bronze,
2. evaluation-based rewards for particularly interesting approaches,
3. competition-based ranking in 6 categories.

1) Achievements

In the RERS challenge achievements

• are given from a verifiers perspective: given answers must be correct, but there is no need to answer every question,
• require are least as many answers as can be witnessed by finite (counter example) paths, i.e., reachable error labels and violated LTL properties. Any kind of answer (yes or no) counts for reaching this threshold, which however is unknown to the participants. Missed detected witness paths can well be compensated for by, e.g., claiming unreachability for other error labels.
• build upon each other, meaning in an achievement category the amount of correct answers for silver subsumes the number of required answers for bronze, and the amount of correct answers for gold subsumes the ones for silver. More concretely, for the gold achievement of a category one needs to provide as many correct answers as there are problems whose solution can be proved by a finite path.

For all kinds of achievement categories, 1) pure, 2) arithmetic, 3) data structure and 4) concurrency (the corresponding problems will be published soon), we have

• a reachability part where

  the number of correct answers to gain the respective achievement corresponds to the number of reachable errors. For example if in the silver category 35 errors are reachable and in all lower problems (bronze and basic) accumulated 70 errors are reachable, you need to have 105 correct answers for that category to gain the silver achievement.

• and a full LTL part where

  the number of correct answers to gain the respective achievement corresponds to the number of LTL properties that can be disproved by a finite counterexample trace. For example, if in the silver problem of a category 35 LTL formula are unsatisfied and in all lower problems (bronze and basic) accumulated 70 LTL formula are unsatisfied, you need to have 105 correct answers for that category to gain the silver achievement.

Thus it is possible to gain eight achievements. In addition, we will publish four additional, particularly hard problems in July which are rated in the same fashion but independently.
Please note that a single incorrect answer spoils the whole achievement.

2) Evaluation-Based Rewarding

In this category rewarding is done according to the employed (combination of) methods (which must not necessarily have scored highest). The submitted descriptions of approaches and 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 price for the best conceptual contribution is a gift certificate for Springer books sponsored by Springer.

3) Competition-based Ranking

The competition-based ranking builds upon the gained achievements refined by score: competitors may submit a separate solution file which may also contain wrong answers, and whose score is evaluated by giving one point for each correct answer, but subtracting two points for each wrong answer (correct = +1, wrong = -2, and open = 0).

Additionally, there is an overall ranking according to the olympic medal ranking of countries, which can be regarded as being lexicographic in gold, silver and bronze, again refined using the scores.
The price for the winners of each of these rankings is a gift certificate for Springer books sponsored by Springer.