• 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


To generalize the solution format only "true" and "false" are allowed as answers. The property should always be specified as a number. Please remember this and adapt your scripts!

Submission for RERS 2017 problems

Submission is possible until 01/07/17 anytime on earth. Please send your submission via email including the following information:
  • The version(s) that you used
    • Sequential: C99 or Java
    • Parallel: Process graphs, Promela, or Petri nets
  • Your solutions as a comma separated value (CSV) file, or as a ZIP/TAR archive (see details below)
  • Your submissions for the evaluation based ranking as a pdf file (optional)
  • Your name
  • Your affiliation (optional)
  • Names (and optionally, also affiliations) of co-authors of the submission
  • A statement whether or not you would like to participate in the ranking-based competition (and in case you do, whether you would like to opt-out of individual track categories)
  • A list of used tools that are available online (using other people's tools is fine. This information allows us to distinguish tool authors from other users)

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:



  • no is the problem specification number.
  • spec is the property specification identifier, where number 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.