The RERS Workshop 2017 program is available here. The workshop is co-located with the ISSTA and SPIN conferences and will be held on July 12th in Santa Barbara, CA, USA.

Rigorous Examination of Reactive Systems (RERS)

The RERS Challenge 2017 is the 7th International Challenge on the Rigorous Examination of Reactive Systems and is co-located with the SPIN Symposium 2017. The event will be held on July 12th 2017 in Santa Barbara, California, USA. 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 to tens of thousands lines of code), to contained language features (arrays and index arithmetic). 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 the only challenge with a special track for LTL analysis on synthesized benchmarks.

The main aims of RERS 2017 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

Contact

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 2017 Organizers

Scientific committee:
• Falk Howar, Institute for Applied Software Systems Engineering, Germany
• Markus Schordan, Lawrence Livermore National Laboratory, CA, USA
• Bernhard Steffen, Technische Universität Dortmund, Germany
• Jaco van de Pol, University of Twente, the Netherlands
Benchmark generation committee:
• Sequential benchmarks: Maren Geske, Technische Universität Dortmund, Germany
• Parallel benchmarks: Marc Jasper, Technische Universität Dortmund, Germany
Publicity committee:
• Jeroen Meijer, University of Twente, the Netherlands

Important Dates

• 01/02/17: Release of training problems
• 15/02/17: Release of properties and benchmarks problems
• 01/03/17: Release of parallel training problems
• 26/05/17: Release of parallel problems
• 01/02/17 - 01/07/17: Challenge Phase
• 15/02/17 - 01/07/17: Submission of solutions
• 12/07/17: Presentation of results at the Spin Symposium