• Jan. 12th, 2021:
        Results online
  • Oct. 2nd, 2020:
       Parallel problems released
  • Sept 8th, 2020:
       Submission dates changed    (see below)
  • July 27th, 2020:
       Sequential challenge    problems released. Parallel    problems will follow soon.
  • July 17th, 2020:
       Submission dates changed    (August → September)
  • May 18th, 2020:
       Sequential training problems    released
  • May 5th, 2020:
       Important dates announced

Important Dates:

  • Dec. 14th, 2020:
       RERS event (held virtually)
  • Nov. 15th, 2020:
       Submission, parallel tracks
  • Oct. 9th, 2020:
       Final submission, sequential
  • Oct. 2nd, 2020:
       Initial submission, sequential
  • Oct. 2nd, 2020:
       Parallel problems
  • July 27th, 2020:
       Sequential problems
  • May 18th, 2020:
       Training problems

Sequential Training Problems

The problems listed here represent smaller versions of the actual problems used during the RERS Challenge 2020. Problems 1 – 3 resemble problems from the Sequential LTL track. As with the challenge problems, C99 and Java versions are available for each training problem.

This year, we have fine-tuned the depth of LTL counterexamples, meaning the number of steps required to falsify a given property, based on a newly conceived approach for safety properties. Therefore, the new training problems below only feature safety properties. Actual challenge problems might also include other properties. For examples, please consider looking at training problems from previous RERS iterations such as 2019.

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.

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.
  • .constraints-... (.txt file): LTL properties that participants of RERS have to check on the given program. See the problem description for details.
  • constraints-solution-... (.txt file): Lists the correct "true"/"false" answers for each property, including exemplary counterexample traces for violated properties. This will not be available for actual challenge problems.

plain, small arithmetic, small data structures, small
Problem1 Problem2 Problem3

Reachability Training Problems

Please use the training problems from previous challenge iterations, for example those from RERS 2019.