• 10/04/15 Results up
• 10/02/15 Solutions for challenge up
• 09/05/15 RV traces and ext. file released
• 08/26/15 Submission opened, RV dates updated
• 07/18/15 RV training traces
• 05/15/15 Training solutions up

## Important Dates:

• 05/15/15
Solutions Training Phase
• 08/01/15 - 09/04/15
White Box Submission
• 09/05/15
Release Monitoring Input
• 09/08/15
RV Submission

## Rewards and Achievements

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 for each category.

### 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, 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 a gold achievement 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, 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 for a silver problem 35 errors are reachable and in all lower problems (bronze) accumulated 40 errors are reachable, you need to have 75 correct answers 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 a silver problem 35 LTL formula are unsatisfied and in all lower problems (bronze) 40 LTL formula are unsatisfied, you need to have 75 correct answers to gain the silver achievement.

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 prices will be announced shortly.

### 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). The prices will be announced shortly.