• Apr. 18, 2019:
        Results online
  • Mar. 13, 2019:
        C code of industrial training     problems and reachability
        problem m106 updated
  • Mar. 09, 2019:
       IMPORTANT: C99 code of    sequential and industrial    challenge problems replaced
  • Feb. 27, 2019:
       Parallel LTL/CTL problems &     training problems released
  • Feb. 01, 2019:
       Sequential and industrial
       challenge problems released
  • Feb. 01, 2019:
       Parallel challenge problems    will be released asap
  • Jan. 25, 2019:
       Training problems
       now available

Important Dates:

  • Apr. 06 – 7, 2019:
       RERS at TACAS'19
  • Mar. 22, 2019:
       Solution submission
  • Feb. 01, 2019:
       Release of challenge
  • Jan. 25, 2019:
       Training problems

Rewards and Achievements


Successful participants of RERS can earn monetary rewards and gift certificates. With the exception of a singe reward for the evaluation-based award, these prizes are only given out based on the competition-based ranking (see below). The following prizes are available during RERS 2019:

  • Industrial tracks (LTL/CTL/Reachability):
    For each of these three tracks, ASML and ESI sponsor up to 1000 Euros as prize money. The team with the winning submission (highest score in the ranking) receives 600 Euros. The second place receives 300 and the third place 100 Euros.
  • Sequential tracks (LTL/Reachability) and parallel tracks (LTL/CTL):
    In each of these four tracks, the winner (highest ranking score) receives a 250 Euro gift certificate for Springer books.
  • 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 the evaluation-based award (see below). This award is also accompanied by a 250 Euro gift certificate for Springer books.

Evaluation Scheme

Note to previous participants (ranking):
Unreachable errors and verifiable LTL properties are now worth twice as many points as before (and four times as many when answered incorrectly).

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.
  • Parallel tracks:
    Achievements of the Parallel LTL track work like in the sequential tracks. For the Parallel CTL track, 12 out of 20 properties mark the threshold for an individual problem (instead of the number of refutable properties). Let n be the number of problems in the Parallel CTL track. Then for the Bronze achievement for example, 12 * (n / 3) properties need to be answered correctly.
  • Industrial tracks:
    Within each track and each of the two contained categories (arithmetic and data structures), the awarded achievement level depends on the number of solved problems. If a participant succesfully solves 1/3 of the problems, then the Bronze Achievement is awarded. Similarly, Silver requires 2/3 of the problems to be solved and Gold requires all problems of that category in that given track.
    A problem is counted as solved if the corresponding threshold of correct answers is reached and if no wrong answers where given regarding its properties. The threshold for solving a problem depends on the track:
    • LTL and Reachability tracks:
      The number of correct answers to solve a given problem is equal to the number of refutable properties (falsifiable LTL/reachable errors).
    • CTL track:
      The number of correct answers to solve a given problem is equal to 12.

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 problem, 20 per problem during other tracks), 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
  • CTL: 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.