• Jan. 12th, 2021:
        Results online
  • Oct. 2nd, 2020:
       Parallel problems released
  • Sept 8th, 2020:
       Submission dates changed    (see below)
  • July 27th, 2020:
       Sequential challenge    problems released. Parallel    problems will follow soon.
  • July 17th, 2020:
       Submission dates changed    (August → September)
  • May 18th, 2020:
       Sequential training problems    released
  • May 5th, 2020:
       Important dates announced

Important Dates:

  • Dec. 14th, 2020:
       RERS event (held virtually)
  • Nov. 15th, 2020:
       Submission, parallel tracks
  • Oct. 9th, 2020:
       Final submission, sequential
  • Oct. 2nd, 2020:
       Initial submission, sequential
  • Oct. 2nd, 2020:
       Parallel problems
  • July 27th, 2020:
       Sequential problems
  • May 18th, 2020:
       Training problems


The RERS Challenge 2020 has concluded with the formal announcement of the winners at the RERS event 2020 that was held as a virtual event this year. 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 (see available tracks) were considered. For more details on the evaluation, please refer to the challenge rules.

List of participants

  • Inria & ISTI-CNR
    Frédéric Lang & Franco Mazzanti & Wendelin Serwe
    Inria, Grenoble, France & ISTI-CNR, Pisa, Italy
    Tools: CADP (developer), PMC (developer), KandISTI/FMC (developer)
  • LLNL
    Markus Schordan
    Lawrence Livermore National Laboratory, USA
    Tools: CodeThorn/ROSE (developer)
  • LMU Munich
    Karlheinz Friedberger
    LMU Munich, Germany
    Tools: CPAchecker (developer)
  • NUS & NITW & Huawei
    Joxan Jaffar & Sangharatna Godboley & Rasool Maghareh
    National University of Singapore, Singapore & National Institute of Technology Warangal, India & Huawei Heterogeneous Compiler Lab, Toronto, Canada
    Tools: Tracer-X (developer), Frama-C
  • RWTH Aachen
    Joshua Moerman & Philipp Berger
    RWTH Aachen University, Germany
    Tools: LearnLib, NuSMV, hybrid-ads, afl-fuzz, Frama-C
    Links: description, repository
  • TU Delft
    Tom Catshoek & Sicco Verwer
    Delft University of Technology, Netherlands
    Tools: AFL++, libFuzzer, NuSMV


The following table shows the achievement certificates that were earned by participants of RERS 2020.

          Category           Inria & ISTI-CNR LLNL LMU Munich NUS & NITW & Huawei RWTH Aachen TU Delft
Sequential Reachability:
Sequential Reachability:
Sequential Reachability:
Data Structures
Sequential LTL:
Sequential LTL:
Sequential LTL:
Data Structures
Parallel CTL:
Parallel CTL:
Parallel CTL:

Ranking evaluation

The following tables list the results of the RERS 2020 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

RankNameScoreWrong answers
2NUS & NITW & Huawei7140
3RWTH Aachen6830
4LMU Munich3120
5TU Delft2480

Sequential LTL: Track ranking

RankNameScoreWrong answers
1TU Delft1230
2RWTH Aachen1162

Parallel CTL: Track ranking

RankNameScoreWrong answers
1Inria & ISTI-CNR790

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 CTL