Important Dates:

  • Oct. 20th – 30th, 2020:
       RERS at ISoLA'20
  • Aug. 20th, 2020:
       Final submission
  • Aug. 10th, 2020:
       Initial submission
  • July 27th, 2020:
       Challenge problems
  • June 1st, 2020:
       Parallel training problems
  • May 18th, 2020:
       Sequential training problems

The RERS Challenge 2020

Part of ISoLA'20,
Rhodes, Greece, October 20 – 30, 2020

Rigorous Examination of Reactive Systems (RERS)

The RERS Challenge 2020 is the 10th International Challenge on the Rigorous Examination of Reactive Systems and is co-located with ISoLA'20. RERS is designed to encourage software developers and researchers to apply and combine their tools and approaches in a free-style manner to answer evaluation questions for reachability and LTL formulas on specifically designed benchmarks. The goal of this challenge is to provide a basis for the comparison of verification techniques and available tools.

The main aims of RERS 2020 are:

  • Encourage the combination of usually different research fields for better software verification results.
  • Provide a comparison foundation based on differently tailored benchmarks that reveals the strengths and weaknesses of specific approaches.
  • Initiate a discussion for better benchmark generation reaching out across the usual community barriers to provide benchmarks useful for testing and comparing a wide variety of tools.

Each benchmark scenario (set of verification tasks, often simply called "problem") of RERS consists of a reactive system in some specification or programming language and a set of properties that participants need to check on that given system. Participants of RERS only need to submit their proposed solutions to these verification tasks. A submission of a tool is not required. What distinguishes RERS from other challenges is that these benchmark scenarios can be approached in a free-style manner: It is highly encouraged to combine any known and newly conceived approaches to software verification. In particular, participants are not constrained to their own tools.

Available Tracks

The main tracks of RERS 2020 are similar to those from last year and include:
  • Sequential LTL
  • Sequential Reachability
  • Parallel LTL
  • Parallel CTL

Compared to previous challenge iterations, the underlying benchmark generation has changed to better fine-tune the hardness of individual verification tasks.

Ways to Publish Results

For participants of the challenge, RERS 2020 offers three different possibilities to feature their approaches in peer-reviewed publications:
  • Full paper (about 15 pages): For those who intend to present their research results based on the RERS challenge in a full paper, the ISoLA'20 track on Software Verification Tools accepts corresponding submissions. The deadline for those submissions is June 30, 2020.
  • Short paper (about 4 pages): If you intend to contribute a brief summary of your approach and corresponding results, please submit your short paper to the RERS track of ISoLA'20 by July 31, 2020.
  • Brief description: To allow us to cover your approach in our summary of RERS 2020, please provide us with a brief description (about 10 lines) and send it along with your initial submission by Aug. 10, 2020. This description can be updated with your final submission by Aug. 20. 2020.


For any questions and inquiries, please contact us at info@rers-challenge.org.

RERS 2020 Organizers

    Scientific committee: Benchmark generation committee:
    • Sequential benchmarks: Malte Mues, Technische Universität Dortmund, Germany
    • Parallel benchmarks: Marc Jasper, Technische Universität Dortmund, Germany