Dear colleagues, The *RERS Challenge* *2017*: is the 7th International
Challenge on the Rigorous Examination of Reactive Systems and is *co-located
with ISSTA/SPIN 2017*. The event will be held in *July 2017, in Santa
Barbara, 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 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 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 There
will be a 1 day workshop where the results will be presented, the
generation methodology will be explained, and the modalities for the RERS
2018 challenge, which will be part of ISoLA 2018 will be discussed. There
is still a lot of time to get engaged, and collecting RERS achievements is
a lot of fun! In addition there will be book prices sponsored by Springer.
Schedule: ========= SEQUENTIAL PROBLEMS =================== The sequential
challenge just started. Its entire setup in online since a few days. Thus
you can start right away. At least if you are a RERS newcomer, we would
strongly recommend you to start with the training problems: (
http://www.rers-challenge.org/2017/index.php?page=trainingphase) They are
an ideal starting point for the challenge: They are smaller in size than
the challenge problems but otherwise structurally equivalent. Moreover, an
automatic checker (available on the same page) allows you to evaluate your
own solutions. After having tackled the training problems it should be easy
to move on to attack the challenge problems. PARALLEL PROBLEMS
================= 01.03.2017: The training problems for the parallel
challenge wil be online 01.05.2017: The setup for the parallel challlenge
will be online. *DEADLINE for all submission* ===========================
*01.07.2017*   Please note that we want to specifically encourage also
solutions from participants that work with tools developed by others. More
detailed information on the challenge can be found in the participants
section of www.rers-challenge.org/2017. Looking forward to seeing you in
Santa Barbara! Best regards Bernhard, Falk, Jaco, and Markus