Results
The RERS Challenge 2019 has concluded with the formal announcement of the winners at the RERS event 2019,
co-located with TOOLympics (TACAS'19).
On this page we present the 4 teams that participated in this year's challenge and list the corresponding results.
In order to provide a more fine-grained view of the results, we also display ranking results per category for those teams who participated in the ranking.
For the competition however, only the results per track (see available tracks) were considered. For more details on the evaluation, please refer to the challenge rules.
List of participants
- ACMU@ISI
Animesh Basak Chowdhury
ACMU, Indian Statistical Institute, India
Tools: American Fuzzy Lop, Instrim, LLVM Interval Analysis - ISTI & Inria
Franco Mazzanti & Frédéric Lang
ISTI-CNR, Italy & Inria-LIG/CONVECS, France
Tools: CADP (developer), KandISTI (developer), nuXmv - LLNL
Markus Schordan
Lawrence Livermore National Laboratory, USA
Tools: CodeThorn/ROSE (developer) - LMU Munich
Karlheinz Friedberger
LMU Munich, Germany
Tools: CPAchecker (developer)
Achievements
The following table shows the achievement certificates that were earned by participants of RERS 2019.
| Category | ACMU@ISI | ISTI & Inria | LLNL | LMU Munich |
| Sequential Reachability: Plain |  |
 |
|
|
| Sequential Reachability: Arithmetic |  |
|
|
|
| Sequential Reachability: Data Structures | |
|
||
| Sequential LTL: Plain | |
|||
| Sequential LTL: Arithmetic | |
|||
| Sequential LTL: Data Structures | |
|||
| Industrial Reachability: Arithmetic | |
|
||
| Parallel LTL: Small | |
|||
| Parallel LTL: Medium | |
|||
| Parallel LTL: Large | |
|||
| Parallel CTL: Small | |
|||
| Parallel CTL: Medium | |
|||
| Parallel CTL: Large | |
Ranking evaluation
The following tables list the results of the RERS 2019 ranking evaluation. Drop-down lists below the tables allow to view ranking results for each category individually (if available). Note that these category-specific scores did not influence the ranking and are provided as additional information. Only the scores for each track were considered during the ranking. Note that a team's track score may be different from the sum of all corresponding track categories due to the non-linear penalty for wrong results.
For detailed information about the solved properties you can download a .zip archive that contains the (syntactically normalized) answers of those who participated in the ranking as well as the official solutions.
Sequential Reachability: Track ranking
| Rank | Name | Score | Wrong answers |
| 1 | LLNL | 669 | 0 |
| 2 | LMU Munich | 306 | 0 |
| 3 | ACMU@ISI | 217 | 0 |
Sequential LTL: Track ranking
| Rank | Name | Score | Wrong answers |
| 1 | LLNL | 881 | 0 |
Industrial Reachability: Track ranking
| Rank | Name | Score | Wrong answers |
| 1 | ACMU@ISI | 2038 | 10 |
| 2 | LMU Munich | 1262 | 0 |
Parallel LTL: Track ranking
| Rank | Name | Score | Wrong answers |
| 1 | ISTI & Inria | 270 | 0 |
Parallel CTL: Track ranking
| Rank | Name | Score | Wrong answers |
| 1 | ISTI & Inria | 180 | 0 |
The following drop-down lists allow you to view the ranking evaluation for individual categories. Please click "view!" once selected.