• 26/07/17 results and solutions uploaded
  • 12/06/17 parallel problems updated
  • 26/05/17 parallel problems released
  • 01/03/17 parallel training problems released
  • 15/02/17 sequential problems released
  • 01/02/17 training sequential up, challenge problems postponed
  • 27/01/17 update on parallel problems

Important Dates:

  • 12/07/17
  • 01/02/17
       Release Sequential Training    Problems
  • 15/02/17
       Release Sequential    Problems
  • 01/03/17
       Release Parallel Training    Problems
  • 26/05/17
       Release Parallel Problems
  • 01/02/17 - 01/07/17
       Challenge Phase
  • 15/02/17 - 01/07/17
       Solution Submission

Rewards and Achievements

RERS has a 3-dimensional reward structure:

  1. Achievement certificates in gold, silver and bronze for each category of each track.
  2. Evaluation-based rewards 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.
  • 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 (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 (Bronze, Silver, and Gold), only the most difficult achievement in a category is reported. In total there are 8 achievement categories: 3 categories within each of the two tracks Sequential Reachability and Sequential LTL, as well as 2 categories in the Parallel LTL track.
    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 category "State Space" from the Parallel LTL track however features problems 110 and 111 as bronze, 112 and 113 as silver, and 114 and 115 as gold problems. 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.

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

2) Evaluation-Based Rewards

Two times 250 Euro in gift certificates for Springer books available, for the best contribution in the sequential tracks and for the best contribution in the parallel track

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 email your contribution as a pdf file. Each participant is invited to shortly present his or her approach to solve the challenge problems at the RERS meeting.

3) Competition-Based Ranking

Three times 250 Euro in gift certificates for Springer books available, for the winners of each track

There is a separate competition-based ranking for each of the three separate tracks Sequential Reachability, Sequential LTL, and Parallel LTL. It is possible to opt-out of the competition-based ranking (overall or in individual tracks), but prices are only provided to 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 that track combined. (correct = +1, wrong = exponential penalty for all n mistakes of 2 to the power of n, and not submitted = 0).