Important Dates:

  • July 31th, 2022:
       Final submission, sequential
  • May 31st, 2022:
       Sequential problems
  • April 4th, 2022:
       Training problems

Rewards and Achievements


Successful participants of RERS can earn gift certificates for Springer books. In each of these tracks, the winner (highest ranking score, see below) receives a 200 Euro gift certificate for Springer books. A similar reward is dedicated to the evaluation-based award: Based on the optional submission of a description (.pdf document) that documents a participant's approach, a committee selects one interesting contribution for this category (see below).

Evaluation Scheme

RERS has a trifold reward structure:

  1. Achievement certificates in gold, silver and bronze for each category of each track.
  2. Evaluation-based awards for particularly interesting approaches.
  3. Competition-based ranking for each track separately for those interested.
Participation in each of these reward categories is optional. In addition, achievements are awarded per category, and only earned achievements will be listed in the results. If you are a tool developer you should name your tool with the submission and it will be displayed for the achievements and ranking on the website. The separation between tool developers and users will be highlighted.

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.

Achievements are only awarded to a participant in a specific category if he or she did not submit wrong answers in that category. Achievements are based on different thresholds that depend on the type of track:

  • Sequential tracks:
    • Require at least as many answers as can be witnessed by (counterexample) paths for each problem/achievement, i.e., reachable error labels and violated LTL properties. Any kind of answer ("true" or "false") counts for reaching this threshold, which however is unknown to the participants. In the Sequential Reachability track for example, undetected error witnesses can be compensated for by claiming unreachability of other error labels (if those are actually unreachable).
    • Build upon each other (Bronze, Silver, and Gold): Only the most difficult achievement in a category is reported. For example, there are 3 categories within each of the two tracks Sequential Reachability and Sequential LTL.
      The thresholds for Gold, Silver, and Bronze Achievements are defined as follows for each category:
      T_Bronze=#falsifiable properties of bronze problems
      T_Silver=T_Bronze + #falsifiable properties of silver problems
      T_Gold=T_Silver + #falsifiable properties of gold problems

      Which benchmark corresponds to the threshold of what achievement level (Bronze, Silver, Gold) can be seen in the illustrations on the respective download page. For example, each category from the Sequential Reachability and Sequential LTL tracks consists of one problem per medal value. The participant's score S is computed from all submitted correct verification/falsification results for each category separately.
      Example: Let participant_score("Plain") = #submitted_properties("Plain",bronze_problems) + #submitted_properties("Plain",silver_problems) + #submitted_properties(plain,gold_problems). If participant_score >=T_Bronze and participant_score < T_Silver, then the participant is awarded the Bronze Achievement in the "Plain" category if he or she only submitted correct results in that category.

2) Evaluation-Based Award

In this category winners are chosen 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 organizers. Due to the possible variety of methods there may be several winners in this category. Please submit your contribution as a pdf file according to the submission page. Each participant is invited to shortly present his or her approach to solving the challenge problems at the RERS event.

3) Competition-Based Ranking

There is a separate competition-based ranking for each track. It is possible to opt-out of the competition-based ranking (overall or in individual tracks).

The scoring for the competition-based ranking can be explained based on the idea of collected tokens. Each participant possesses two tokens counters: A counter for correct answers ("correct tokens") and one for incorrect answers ("incorrect tokens").

For each answer to an individual property (100 for each sequential reachability problem, 10 for each sequential LTL problem), a participant collects tokens that are accumulated in either of these two counters, depending on whether or not the answer was correct. Unanswered properties (or "unknown" answers) are ignored; No tokens are collected in this case. Answers are worth the following amount of tokens:

  • Verifiable LTL or unreachable error: Two tokens
  • Refutable LTL or reachable error: One token
After counting all tokens that a participant collected within a given track, let p be the number of correct tokens and q the number of incorrect tokens. Then the final score of this participant is p - q2.