The RERS Challenge
RERS 2022
Part of ISoLA'22,
Rhodes, Greece, October 24 – November 3, 2022
Rigorous Examination of Reactive Systems (RERS)
Reactive systems appear everywhere, e.g. as Web services, decision support systems, or logical controllers. Their validation techniques are as diverse as their appearance and structure. They comprise various forms of static analysis, model checking, symbolic execution and (model-based) testing, often tailored to quite extreme frame conditions. Thus it is almost impossible to compare these techniques, let alone to establish clear application profiles as a means for recommendation. The RERS Challenges aim at overcoming this situation by providing a forum for experimental profile evaluation based on specifically designed benchmark suites. These 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. reachablity, full safety, liveness), over size of the reactive systems (a few hundred lines to millions of them), to exploited language features (arrays, arithmetic at index pointer, and parallel message passing).
Characteristic for RERS is its wide scope, which addresses not only source code analyzers, but also (model-based) testers and (test-based) modelers, and in particular free-style approaches.
A leading goal is to investigate the power of and synergy potential between source code-based (White-Box) approaches and purely testing-based (Black-Box) approaches:
- How much does the source code of historically grown legacy applications help?
- How far carries a purely testing-based investigation?
- What is a good way to combine the two?
Testing-based approaches are independent of language features, but, to quote Dijkstra, they can only proof the presence of errors, never their absence. Source code analysis has the power to proof the absence of errors, but each new language feature may requires an enormous effort. Realistic problems will most probably always require both approaches, which, today, are typically applied in isolation.
The RERS Challenge provides a wealth of problems of increasing complexity, the more involved of which will probably be beyond any individual state-of-the-art method or tool. In order to encourage cooperation and the consideration of alternative solutions, the RERS Challenges follow a clear free-style philosophy: Apply whatever approach you consider to be valuable, be it one that is already available or one that you are willing to specifically conceive/implement.
Latest challenges
In addition to tracks on synthesized sequential and parallel programs, RERS 2019 inlcudes new tracks featuring industry-based programs.
Overall, the challenge features CTL, LTL, and Reachability properties. It is co-located with TACAS 2019 and takes place in Prague, Czech Republic.
More details about RERS 2019 can be found here. |
The challenge features two tracks for sequential benchmarks, LTL and Reachability, as well as LTL and CTL tracks for parallel benchmarks.
RERS 2018 is co-located with ISoLA 2018 and takes place in Limassol, Cyprus. More details about RERS 2018 can be found here. |
The challenge has two sections for sequential benchmarks, LTL and Reachability, and an LTL section for parallel benchmarks.
The challenge is colocated with ISSTA/SPIN 2017 and takes place in Santa Barbara, CA, USA. More details about RERS 2017 can be found here. |
