• 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

How to Proceed

To get a feeling for the provided problems, we provide a set of sequential, industrial, and parallel training problems with solutions that are very similar to those found in the actual challenge, but tend to be smaller in size.

You may proceed as follows:

  • Step 1. Download the sequential, industrial, or parallel training problems of the track that you want to participate in.
  • Step 2. Read the sequential, industrial, or parallel problem description. Select your favorite method or tools to find out which properties are satisfied. You may use your own tool or other people's tools or any combination thereof - the challenge is completely free-style. Some prominent tools you may consider to involve are:
    1. CADP
    2. LearnLib
    3. LTSmin
    4. mCRL2
    5. SPIN
    If you would like your tool to be listed here or if you have any other suggestion for tools, please contact us.
  • Step 3. Test the success of your methods or tools using the sequential, industrial, or parallel training problems.
  • Step 4. Once you are warmed up by working with the training problems, you will be ready for the actual challenge. Repeat Step 1 to Step 3 for the challenge problems. Good luck!
  • Step 5. Submit your solutions within the provided time frame for each category as listed on the left. The submission format is defined on the submission page.
  • Step 6. Receive your evaluation and hopefully also your achievements and rewards during the RERS event. At this event, we will also discuss the profile of future RERS problems.

The challenge is free-style. You are allowed to patch the code in any way you like, but the validity has, of course, to be stated according to the original problems. Nevertheless, it is advisable to first focus on the problems and properties that you can solve well. You do not have to give an answer to all properties within a problem. Of course, the more problems you can tackle, the more points you may be able to earn, but please be aware that wrong answers have a high penalty.

Apart from achievements and the ranking, RERS features an evaluation-based award. In order to participate in this category, please write a brief summary of your approach, the encountered hurdles, your solutions, and your results. In these summaries, honesty, e.g. also concerning weaknesses of the employed methods, is important. Our challenge aims at profiling the various approaches and methods, which in particular means that weaknesses need to be identified. Of course, we are also very interested in new ideas and solutions that were motivated by the challenge. Details about the ranking or evaluation method can be found here.