• 22/10/16 Solutions uploaded
  • 20/08/16 Parallel problems replaced
  • 07/08/16 Parallel problems released
  • 20/06/16 workshop date annouced
  • 13/06/16 Parallel release announced
  • 01/05/16 Problems up

Important Dates:

  • 09/10/16
       RERS workshop at ISoLA
  • 31/05/16
       Release Ranking Details
  • 01/05/16 - 15/09/16
       Challenge Phase
  • 01/09/16 - 15/09/16
       Solution Submission
  • 07/08/16 - 15/09/16
       Release Parallel Problem

The RERS Challenge 2016

part of ISoLA'16, Corfu, Greece, October 05 - 14th 2016

The RERS workshop will take place in the afternoon on the 9th of October 2016 at ISoLA.

Rigorous Examination of Reactive Systems (RERS)

The RERS Challenge 2016 is the 6th International Challenge on the Rigorous Examination of Reactive Systems and is co-located with ISoLA 2016. The event will be held in October 2016, in Corfu, Greece. 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 benchmarks are automatically synthesized to exhibit chosen properties and then enhanced to include dedicated dimensions of difficulty, ranging from conceptual complexity of the properties (e.g. reachability, full safety, liveness), over size of the reactive systems (a few hundred lines to tens of thousands of them), to exploited language features (arrays and index arithmetics). They are therefore especially suited for community-overlapping tool comparisons. What distinguishes RERS from other challenges is that the challenge problems can be approached in a free-style manner: it is highly encouraged to combine and exploit all known (even unusual) approaches to software verification. In particular, participants are not constrained to their own tools. To clearly separate RERS from other challenges, this year the LTL analysis is separated from the reachability of labels. RERS is then the only challenge with a special track for LTL analysis on synthesized benchmarks.

The main aims of RERS 2016 are to :

  • 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


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

If you wish to receive news and important information about the current challenge you can subscribe to our announcement google group! Upcoming challenges or changes to deadlines will broadcasted over this group. If you wish to give feedback on the challenge, or discuss what should be part of future challenges you can subscribe to our discussion google group!

RERS 2016 Committee

Benchmark generation and administration:
Maren Geske, Technische Universit├Ąt Dortmund, Germany

Important Dates

  • 01/05/16: Release of properties and benchmarks problems
  • 31/05/16: Release of details for the ranking and rewards
  • 01/09/16 - 15/09/16: Submission of solutions for LTL and reachability properties
  • 07/08/16: Release of a parallel problem
  • 09/10/16: Presentation of results at ISoLA