• 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

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.

RERS Newsletter

In order to stay informed about current RERS announcements, please send an email titled “subscribe” to info@rers-challenge.org. You will then receive an invitation to our current RERS group on Google Groups that also allows to discuss topics related to the challenge.


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