Updates

Important Dates:

  • Nov. 08, 2018:
       RERS at ISoLA'18
  • Oct. 01 – Oct. 14, 2018:
       Solution Submission
  • Aug. 22, 2018:
       Release Parallel LTL
  • Jul. 18, 2018:
       Release Sequential LTL and
       Sequential Reachability
  • Jul. 18, 2018:
       Training benchmarks
       available

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

RankNameScoreWrong answers
1Freiburg3670
2Twente3250
2LLNL3250
3LMU Munich2191

Sequential LTL: Track ranking

RankNameScoreWrong answers
1LLNL6820
2Twente5740

Parallel LTL: Track ranking

RankNameScoreWrong answers
1Twente450

Parallel CTL: Track ranking

RankNameScoreWrong answers
1Aalborg90
2ISTI-CNR80

The following drop-down lists allow you to view the ranking evaluation for individual categories. Please click "view!" once selected.

Sequential Reachability

Sequential LTL

Parallel LTL

Parallel CTL