<div dir="ltr"><br><div><span style="font-family:monospace;font-size:14px;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-alternates:normal;font-variant-east-asian:normal;line-height:normal;white-space:pre-wrap">Dear colleagues, 

The </span><font color="#ff0000" style="font-family:monospace;font-size:14px;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-alternates:normal;font-variant-east-asian:normal;line-height:normal;white-space:pre-wrap"><b>RERS Challenge</b></font><font color="#222222" style="font-family:monospace;font-size:14px;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-alternates:normal;font-variant-east-asian:normal;line-height:normal;white-space:pre-wrap"> </font><font color="#ff0000" style="font-family:monospace;font-size:14px;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-alternates:normal;font-variant-east-asian:normal;line-height:normal;white-space:pre-wrap"><b>2017</b></font><font color="#222222" style="font-family:monospace;font-size:14px;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-alternates:normal;font-variant-east-asian:normal;line-height:normal;white-space:pre-wrap">: is the 7th International Challenge on the Rigorous
Examination of Reactive Systems and is </font><font color="#ff0000" style="font-family:monospace;font-size:14px;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-alternates:normal;font-variant-east-asian:normal;line-height:normal;white-space:pre-wrap"><b>co-located with ISSTA/SPIN 2017</b></font><font color="#222222" style="font-family:monospace;font-size:14px;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-alternates:normal;font-variant-east-asian:normal;line-height:normal;white-space:pre-wrap">. The
event will be held in </font><font color="#ff0000" style="font-family:monospace;font-size:14px;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-alternates:normal;font-variant-east-asian:normal;line-height:normal;white-space:pre-wrap"><b>July 2017, in Santa Barbara, USA</b></font><font color="#222222" style="font-family:monospace;font-size:14px;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-alternates:normal;font-variant-east-asian:normal;line-height:normal;white-space:pre-wrap">. 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:
(</font><a class="gmail-m_2119434015525247858moz-txt-link-freetext" href="http://www.rers-challenge.org/2017/index.php?page=trainingphase" target="_blank" style="font-family:monospace;font-size:14px;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-alternates:normal;font-variant-east-asian:normal;line-height:normal;white-space:pre-wrap">http://www.rers-challenge.<wbr>org/2017/index.php?page=<wbr>trainingphase</a><font color="#222222" style="font-family:monospace;font-size:14px;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-alternates:normal;font-variant-east-asian:normal;line-height:normal;white-space:pre-wrap">)
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.


</font><font color="#ff0000" style="font-family:monospace;font-size:14px;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-alternates:normal;font-variant-east-asian:normal;line-height:normal;white-space:pre-wrap"><b>DEADLINE for all submission</b></font><font color="#222222" style="font-family:monospace;font-size:14px;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-alternates:normal;font-variant-east-asian:normal;line-height:normal;white-space:pre-wrap">
===========================
</font><font color="#ff0000" style="font-family:monospace;font-size:14px;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-alternates:normal;font-variant-east-asian:normal;line-height:normal;white-space:pre-wrap"><b>01.07.2017</b></font><font color="#222222" style="font-family:monospace;font-size:14px;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-alternates:normal;font-variant-east-asian:normal;line-height:normal;white-space:pre-wrap">
 
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
</font><a class="gmail-m_2119434015525247858moz-txt-link-abbreviated" href="http://www.rers-challenge.org/2017" target="_blank" style="font-family:monospace;font-size:14px;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-alternates:normal;font-variant-east-asian:normal;line-height:normal;white-space:pre-wrap">www.rers-challenge.org/2017</a><font color="#222222" style="font-family:monospace;font-size:14px;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-alternates:normal;font-variant-east-asian:normal;line-height:normal;white-space:pre-wrap">.


Looking forward to seeing you in Santa Barbara!

Best regards
Bernhard, Falk, Jaco, and Markus</font><br></div></div>