• 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


Submission is possible until March 22, 2019 anytime on earth.

Important updates (Mar. 13th & 9th):

Please only submit your solutions based on the newest version:

  • Mar. 13th: The C99 code of problem m106 has been replaced (Industrial Reachability track only).
  • Mar. 9th: The C99 code of the sequential and industrial challenge problems has been replaced.

For information on the submission format (.csv file), please click here.

Apart from submitting an optional description of your approach (evaluation-based award), there are three main submission options to choose from:

  • Regular: Achievements will be published if earned. Ranking scores/positions will be published in tracks of your choice.
  • Achievements only: Achievements will be published if earned. No participation in the ranking.
  • Anonymous: Ranking scores attributed to a generic participant name. No achievements.
Please use the following template to send us an email with your submission file(s) to info@rers-challenge.org. Note that depending on your chosen submission option, this template includes a disclaimer that corresponding results will be published on the RERS website.

Submission E-Mail Template

Dear RERS organizers,

Attached to this e-mail you can find our/my submission to the RERS Challenge 2019.

In addition, please find a description of our approach attached as a .pdf-file (submission regarding the evaluation-based award).

Participant information:
  • Name_1 (<optional> affilation_1 </optional>)
  • Name_2 (<optional> affilation_2 </optional>)
  • ...
We/I used the following problem versions <delete those that do not apply>:
  • Sequential LTL: C99 / Java
  • Sequential Reachability: C99 / Java
  • Industrial LTL: C99 / Java
  • Industrial CTL: C99 / Java
  • Industrial Reachability: C99 / Java
  • Parallel LTL: Promela / Petri net (PNML) / Graphviz (.dot)
  • Parallel CTL: Promela / Petri net (PNML) / Graphviz (.dot)
We/I have used/combined the following tools to generate our submission:
  • Tool_1
  • ...
We/I would like to participate anonymously. We/I are aware that this means that our/my ranking results will be published under a generic name (e.g. “participant A”) on the RERS website and at the RERS event. We/I understand that we/I will not earn any achievements.
We/I have reviewed the different submission options. We/I consent that our/my data corresponding to this submission, including awarded achievements and (if selected) ranking scores, will be published on the RERS website. We/I are/am aware of the possibility to inspect how the results of previous iterations of the RERS Challenge are presented online.

We/I would like to participate in the ranking of the following tracks <delete those that do not apply>:
  • Sequential LTL
  • Sequential Reachability
  • Industrial LTL
  • Industrial CTL
  • Industrial Reachability
  • Parallel LTL
  • Parallel CTL
We/I would like to not be mentioned in the ranking.

Best regards,
Name_1, ...

If you have completed all (or some) tasks, we kindly request you to submit your solution in a CSV-style format. Solutions for each of the problems should be specified in the following way:



  • <number> is the problem specification number.
  • <spec> is the property specification identifier, where numbers 0 to 99 correspond to the LTL or Reachability properties for each problem or error number respectively.
  • <answer> expresses whether or not you believe this error label to be reachable, or the respective LTL property to be satisfied as true/false.

Hence, a line in this file for a hypothetical problem 0 and the error label 37 might look like this:

0, 37, true

Please choose a name for each of the CSV- which clearly identifies the respective problem along with an ID uniquely identifying the solution as yours such as "problemX-<id>.csv". You are free to generate one file for each problem or combine all solutions into a global CSV file. If you split your solutions into several files, please provide them as a ZIP or (compressed) TAR archive.