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

Industrial Training Problems

The problems listed below are similar to the challenge problems of the industrial tracks of RERS 2019. As with the challenge problems, C99 and Java versions are available for each training problem.


Important update (Mar. 13th):

The C99 code of all training problems has been replaced.


Within each track (LTL/CTL/Reachability), there are three training problems in the category "arithmetic" and three problems in the category "data structures". In contrast to the challenge problems, both categories are based on the same set of models. LTL and CTL problems are based on the same code/model in a given category whereas reachability problems feature their own version of the code/model.

Reachability properties are encoded in the source code whereas LTL and CTL files are provided as .txt files. In addition to these property specifications, 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 property descriptions.
  • .traces file: Execution logs provided by ASML. See the problem description for details.
  • .aut file: Reference model based on which the source code was generated. This will not be available for actual challenge problems.
  • "solution_..." file: Lists the correct "true"/"false" answers for each property. This will not be available for actual challenge problems.

For further information on these problems, please refer to the problem description and the Java code and C99 code description.

LTL Training Problems

A zip containing the LTL training problems and solutions can be downloaded here.


CTL Training Problems

A zip containing the CTL training problems and solutions can be downloaded here.


Reachability Training Problems

A zip containing the reachability training problems and solutions can be downloaded here.