RERS has a 3-dimensional reward structure:

1. achievement certificates in gold, silver and bronze for each complexity level for sequential prblems.
2. evaluation-based rewards for particularly interesting approaches.
3. competition-based ranking for each track and category separately for those interested.

If you are a tool developer you can name your tool with the submission and it will be displayed for the achievements and ranking on the website, the persons of the team will be named as a subscript. If you mainly use another person's tool or a combination of tools, your name will be displayed for achievements and ranking with the used tools as a small subcript.

1) Achievements (only sequential)

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 (counter example) paths for each problem/achievement, 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, only the most difficult achievement in a complexity level (plain, sarithmetic or data structures) is reported, 6 are possible in total. This means that in the table below you can only gain one achievement for every column!
  The thresholds for Gold, Silver, and Bronze Achievements are defined as follows for each category (Plain,Arith,Struct):
  T_Bronze=#falsifiable properties of small problem
  T_Silver=T_Bronze + #falsifiable properties of medium problem
  T_Gold=T_Silver + #falsifiable properties of large problem
  
  The participant's score S is computed from all submitted correct verification results for each category seperately (sum of S_small+S_medium+S_large in each category plain, arith, struct).
  Example: Let participant_score(plain) = #submitted_properties(plain,small) + #submitted_properties(plain,medium) + #submitted_properties(plain,large). If participant_score >=T_Bronze and participant_score < T_Silver, then the participant is awarded the Bronze Achievement.

For all kinds of achievement categories, 1) pure (easy), 2) arithmetic (moderate, 3) data structure (hard), we have

• a reachability part where the number of correct answers to gain the respective achievement corresponds to the number of reachable errors.
• 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 counterexample trace.

If one answer is incorrect, the achievement cannot be awarded in the respective category.

bronze	silver	gold
plain	plain	plain
arithmetic	arithmetic	arithmetic
data structures	data structures	data structures

2) Evaluation-Based Rewarding

100 Euro available for the best contribution

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 100 Euro gift certificate for Springer books sponsored by Springer. Please email your contribution as a pdf file.

Each participant is invited to shortly present his or her approach on the challenge at the RERS meeting. The winning and further interesting approaches will be invited to publish a paper in an STTT special section on RERS 2016! We would be delighted to publisch all contributions on the website with your consent.

3) Competition-based Ranking

9x 50 Euro available, sequential: 2 overall and one for each category, parallel: 1

There is a separate competition-based ranking for both categories: LTL and Reachability. The competition ranking can be opted out if you do not want to appear in the ranking (for each problem and overall individually), but prices are only provided for openly competing participants. Only one submission for each participant is allowed and used for both the achievement and ranking (if desired). The score is evaluated by giving one point for each correct answer, but subtracting 2 to the power of n where n is the number of mistakes in all benchmarks of the track combined. (correct = +1, wrong = exponential penalty for all mistakes 2 to the power of n, and not submitted = 0).

For better understanding, the table shows a detailed overview of the sequential categories that are each awarded with a 50 Euro gift certificate for Springer books sponsored by Springer for the participant with the most points in that category.

plain	arithmetic	array	overall
LTL	LTL	LTL	LTL
Reachability	Reachability	Reachability	Reachability