Updates

  • 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
       (TOOLympics)
  • Mar. 22, 2019:
       Solution submission
  • Feb. 01, 2019:
       Release of challenge
       problems
  • Jan. 25, 2019:
       Training problems
       available

Download Reachability Problems

Each participating team is invited to briefly present their approach to the RERS benchmarks at the corresponding event.


Important update (Mar. 9th):

The C99 code has been replaced. Please only submit your solutions based on the new version.


Note that these problems cannot be compiled as downloaded because of a missing implementation of the __VERIFIER_error(int). Please read the Java-code and C99-code description for compilation assistance. Other useful information can be found on the problem description page. Training problems are available and feature corresponding solutions.


The problems are provided as a .zip archive.


Sequential Reachability Problems

The following table provides an overview of this year's challenge problems in the Sequential LTL track. Bronze, silver, and gold backgrounds refer to the corresponding achievements.
size plain, simple arithmetic, medium data structures, hard
small Problem11 Problem12 Problem13
medium Problem14 Problem15 Problem16
large Problem17 Problem18 Problem19