Results
The RERS Challenge 2018 has concluded with the formal announcement of the winners at the RERS event 2018,
co-located with ISoLA 2018.
On this page we present the 6 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 (Sequential Reachability, Sequential LTL, Parallel LTL, and Parallel CTL) were considered. For more details on the evaluation, please refer to the challenge rules.
List of participants
- Aalborg
Peter G. Jensen and Jiri Srba
Aalborg University, Denmark
Tools: verifypn/TAPAAL (developer) - Freiburg
Claus Schätzle and Daniel Dietsch
University of Freiburg, Germany
Tools: Ultimate Automizer (developer), Brutalizer (developer), Frama-C - ISTI-CNR
Franco Mazzanti
ISTI-CNR, Italy
Tools: KandISTI/FMC (developer), CADP, SMV - LLNL
Markus Schordan
Lawrence Livermore National Laboratory, USA
Tools: CodeThorn/ROSE (developer) - LMU Munich
Karlheinz Friedberger
LMU Munich, Germany
Tools: CPAchecker (developer) - Twente
Jeroen Meijer and Jaco van de Pol
University of Twente, The Netherlands
Tools: LTSmin (developer), LearnLib
Achievements
The following table shows the achievement certificates that were earned by participants of RERS 2018. Note that achievements were not available for the Parallel CTL track due to its experimental status in 2018.
Category | Freiburg | LLNL | LMU Munich | Twente |
Reachability: Plain | ||||
Reachability: Arithmetic | ||||
Reachability: Data Structures | ||||
LTL: Plain | ||||
LTL: Arithmetic | ||||
LTL: Data Structures | ||||
Parallel LTL: Track |
Ranking evaluation
The following tables list the results of the RERS 2018 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 than 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 answers of those who participated in the ranking as well as the official solutions as .csv files.
Sequential Reachability: Track ranking
Rank | Name | Score | Wrong answers |
1 | Freiburg | 367 | 0 |
2 | LLNL | 325 | 0 |
2 | Twente | 325 | 0 |
3 | LMU Munich | 219 | 1 |
Sequential LTL: Track ranking
Rank | Name | Score | Wrong answers |
1 | LLNL | 682 | 0 |
2 | Twente | 574 | 0 |
Parallel LTL: Track ranking
Rank | Name | Score | Wrong answers |
1 | Twente | 45 | 0 |
Parallel CTL: Track ranking
Rank | Name | Score | Wrong answers |
1 | Aalborg | 9 | 0 |
2 | ISTI-CNR | 8 | 0 |
The following drop-down lists allow you to view the ranking evaluation for individual categories. Please click "view!" once selected.