The RERS Challenge series aims at a systematic investigation, evaluation, comparison, combination and improvement of any kind of methods for the analysis and validation of reactive systems, be they static, dynamic, Black-Box or White-Box. Its second edition, the (RERS Challenge 2012), focused on ECA systems, a popular class of reactive systems, which comprises in particular Web services, decision support systems, and programmable logical controllers (PLCs). Besides their industrial relevance, ECA systems where chosen as they are on the one hand fully 'White-Box': the full Java/C code will be available, but one the other hand have a Black-Box character: being simply one huge loop of guarded commands, the ECA code structure essentially reveals nothing about the implemented functionality. This property was meant to also address competitors who base their validation on execution rather than source code analysis.

The RERS Challenge 2013 builds on last year's experience. It involves more complex code/data structures in order to attract source code analyzers, and it explicitly addresses execution-based analyses by providing Black-Box and Grey-Box scenarios. In particular the latter scenarios are challenging as they profit most from the combination of source code and execution-based analyses. We therefore hope to encourage people working on areas as diverse as

• program analysis and verification,
• symbolic execution,
• software model checking,
• statistical model checking,
• model-based testing,
• inference of invariants,
• automata learning,
• run-time verification,
• monitoring.

to not only apply there 'home' methods, but to investigate how their methods can be improved by combining them with others.

Challenge Problems:

The RERS Challenge 2013 will provide a wealth of Benchmark problems of increasing complexity, the more involved of which will probably be beyond any individual state-of-the-art method or tool. A large set of Benchmarks will be synthesized to exhibit chosen properties, and then enhanced in an automated process to cover dedicated dimensions of difficulty, including:

1. conceptual complexity of the exhibited properties (reachability, safety, liveness),
2. size of the systems (from a few hundred lines of code to millions of them), and
3. language features (arrays, indirect addressing, floating point arithmetics, virtual method calls, recursion).

Automatically generated problems will be presented in these kinds:

• White-Box: i.e. in Java and C,
• Black-Box: as executables, not meant to be textually analyzed,
• Grey-Box: a mixture thereof.

The challenge rules are essentially free style in order include as many participants as possible. They have a numeric part, which allows for a clear ranking in terms of number of correctly answered questions, and a textual part, where competitors are supposed to describe the approach. This part will be evaluated by the RERS committee. Details about the ranking or evaluation method can be found here.

There are five price categories: White-Box, Black-Box, Grey-Box, overall and for the best approach taken (which must not necessarily have scored highest). In addition we will distribute achievement certificates for solutions passing a specific threshold.

Rewards

There will be an overall price and prices for each kind, as well as a price for the best conceptual contribution in form of a gift certificate for Springer books sponsored by Springer. In addition there will be certificates for the first three in each category, and achievement certificates for every team passing the required threshold. Detailed information can be found on the Rewards and Achievements page.

The teams with the best solutions in their categories will be invited for a STTT Special Section summarizing the results of the challenge, and, in particular, presenting the most advanced solutions.