print · source · login   

The Rigorous Examination of Reactive Systems (RERS) challenges

The Rigorous Examination of Reactive Systems (RERS) challenges are a series of program analysis challenges that aim to evaluate the effectiveness of different software verification techniques.

Characteristic for RERS is its wide scope, which addresses not only source code analyzers, but also (model-based) testers and (test-based) modelers. The RERS challenges are free sytle, which means that participants are encouraged to apply and combine their tools and approaches in a free style manner to answer evaluation questions. The goals of the challenges are to provide a basis for the comparison of verification techniques and available tools, and to investigate the power of and synergy potential between source code-based (white box) approaches and black box approaches, such as active automata learning. For this reason, the RERS challenges are a useful tool for driving further development of (hybrid) active automata learning methods.

Participants in recent RERS challenges are evaluated by their ability to answer a set of evaluation questions correctly for a set of increasingly difficult, specifically designed benchmarks. The evaluation questions fall in one of the following categories:

behavioural properties
An execution trace of a challenge system consists of a sequence of inputs and outputs, each from a finite alphabet. For each problem a set of LTL properties are given, for which the participants have to check whether they are satisfied by all traces, or if there are traces that violate them. It is not expected to also provide these traces.
reachability properties
For each problem (i.e. benchmark) a set of reachability properties are implicitly defined by a set of unique erroneous outputs (exceptions or failed assumptions) that were present in the problem's source code. Not all of these error states were reachable, however, and therefore not all erroneous outputs could be produced by the problem's programs. The goal is to classify for each problem which of the erroneous outputs can be produced, i.e. are reachable.

More information on recent RERS challenges, and the actual benchmarks, can be found on their respective websites: