Important Dates:

For Participants

General

Call for Participation [PDF]

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. Looking back on three successful editions, 2010 at ISoLA, 2012 at ISoLA, 2013 at ASE, it is now time for the fourth edition at ISoLA 2014. Formerly focusing mainly on ECA systems, the challenge evolved over introducing various new arithmetic expressions to data structures. The main character of the challenge is that the problems 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 method with guarded commands. The structure revealing nothing about the implemented functionality is a property that was meant to also address competitors who base their validation on execution rather than source code analysis.

The RERS Challenges build on last years experiences. Each time realizing more complex code/data structures in order to attract source code analyzers, but also very huge systems that may be better analyzed with execution-based approaches. We therefore hope to encourage people working on areas as diverse as

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

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

Challenge Problems:

The RERS Challenge usually provides 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 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 thousands 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 (basic, see 2013): in Java and C (from May 15 to Sep 15)
  • White-Box (extended): in Java and C (from July 31 to Sept 15)

The challenge rules are essentially free style in order to 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.