• 22/10/16 Solutions uploaded
  • 20/08/16 Parallel problems replaced
  • 07/08/16 Parallel problems released
  • 20/06/16 workshop date annouced
  • 13/06/16 Parallel release announced
  • 01/05/16 Problems up

Important Dates:

  • 09/10/16
       RERS workshop at ISoLA
  • 31/05/16
       Release Ranking Details
  • 01/05/16 - 15/09/16
       Challenge Phase
  • 01/09/16 - 15/09/16
       Solution Submission
  • 07/08/16 - 15/09/16
       Release Parallel Problem


Call for Participation

The goal for RERS 2016 is to compare all sorts of software verification tools. Participants are welcome to test their tools on the provided benchmarks and even propose certain programming languages and features that should be supported by the benchmarks.

It is planned to support two main tracks on 9 levels of difficulty for sequential benchmarks:

  • verification of safety and liveness properties (100 LTL formulas)
  • verification of reachable labels (100 reachable labels)
Both tracks will be available in Java and C99.

And 10 parallel benchmarks that have to be analyzed for 20 LTL properties and are avaible as a visual DOT and Promela code.

The competition will proceed as follows:

  • Training phase: the participants are invited to test their tools on a provided training problem. To validate their approach, the solutions will be provided at the end of May.
  • Challenge phase: the participants can test their tools on the provided challenge problems and generate their solutions.
  • Evaluation phase: All turned in solutions will be evaluated for the percentage of right answers. Certificates will be provided for all participants reaching a certain threshold of right answers for each problem.

To get a feel of the challenge please look at the how-to, problem description and challenge rules pages. The evaluation thresholds and possible certificates are described on the rewards page.