• 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

Industrial Reachability Problems

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

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.
  • Mar. 9th: The C99 code of all problems has been replaced.

The problems are divided into two categories: Arithmetic and Data Structures. In contrast to the first category, the second one also features arrays in the source code. Achievements can be earned separately in each of these two categories.

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. The rewards page explains the corresponding ranking and achievements as well as available prizes. Training problems with solutions can be downloaded in order to test an approach before submitting to the challenge.

The following files are contained in each problem's directory:

  • .java file: Java version of the source code.
  • .c file: C99 version of the source code.
  • "...alphabet_mapping_C_version.txt" file: Bijection between the integer values in the C99 version and the input/output symbols in the Java file.
  • .traces file: Execution logs provided by ASML. See the problem description for details.

The problems are provided as a .zip archive.

Industrial Reachability Problems

The following lists provide an overview of this year's challenge problems in the industrial tracks. The table contains the problem identifiers for each of the two categories. Note that the problems are not ordered according to difficulty.
Arithmetic Category
m24 m45 m54 m55 m76
m95 m135 m158 m159 m164
m172 m181 m183 m185 m201
Data Structures Category
m22 m27 m41 m49 m65
m106 m131 m132 m167 m173
m182 m189 m190 m196 m199