RERS Challenge 2019 @ TOOLympics

by Jeroen Meijer, Jan. 30, 2019

Rigorous Examination of Reactive Systems (RERS) 2019 @ TOOLympics (co-located with TACAS'19).

Rigorous Examination of Reactive Systems (RERS)


The RERS Challenge 2019 is the 9th International Challenge on the Rigorous Examination of Reactive Systems. It is part of TOOLympics (co-located with TACAS’19).


RERS is designed to encourage software developers and researchers to apply and combine their tools and approaches in a freestyle manner to answer evaluation questions for reachability, LTL, and CTL formulas on specifically designed benchmarks. The goal of this challenge is to provide a basis for the comparison of verification techniques and available tools.


As a new addition, RERS 2019 features industrial tracks in which problems are based on real-world models. This part of the challenge is a collaboration with ASML and ESI, the former being the world’s leading provider of lithography systems for the semiconductor industry. The three corresponding RERS tracks concern LTL, CTL, and Reachability properties.


ASML and ESI sponsor up to 3000 Euros as price money for these new tracks with regard to the competition-based ranking. As during previous years, gift certificates for Springer books will be available for very successful contributions in the remaining tracks and for the evaluation-based award. A total of 5 gift certificates, each worth 250 Euros in Springer books, are available.

For more information please visit:


The Challenge

The challenge consists of three types of problems—sequential, industrial, and parallel problems—that each feature an increasing difficulty. 

·     The sequential problems are available as both Java and C99 sources. Error reachability and LTL properties can be analyzed.

·     The industrial problems are available as Java and C99 code, and additional execution logs are provided. Reachability, LTL, and CTL properties exist. 

·     The parallel problems are available as Promela code, Petri nets (PNML), and parallel transition systems (DOT). These problems feature LTL and CTL properties.

Your solutions can be submitted until March 22, through Participants are invited to briefly present their approach during the RERS meeting at TOOLympics (April 6 – 7). 


Training Phase is open

Training problems (with solutions) are now available on the website. The actual challenge problems are scheduled for release on Feb. 1.


Important Dates

·     25/01/19: Release of training problems

·     01/02/19: Release of challenge problems

·     01/02/19 – 22/03/19: Submission by participants

·     06/04/19 – 07/04/19: Presentation of results at TOOLympics

RERS 2018 Organizers


·     Scientific committee:

o   Falk Howar, Technische Universität Dortmund, Germany

o   Ramon Schiffelers, Eindhoven University of Technology & ASML, Netherlands

o   Markus Schordan, Lawrence Livermore National Laboratory, CA, USA

o   Bernhard Steffen, Technische Universität Dortmund, Germany

o   Frits W. Vaandrager, Radboud University, Netherlands

o   Jaco van de Pol, Aarhus University, Denmark

·     Benchmark generation committee:

o   Sequential benchmarks: Malte Mues, Technische Universität Dortmund, Germany

o   Parallel benchmarks: Marc Jasper, Technische Universität Dortmund, Germany

o   Industrial benchmarks:

§  Dennis Hendriks, ESI (TNO), Netherlands

§  Harco Kuppens, Radboud University, Netherlands

·     Publicity committee:

o   Jeroen Meijer, University of Twente, the Netherlands

For any questions and inquiries, please contact us at [email protected].