Call for Participation

The goal of RERS 2017 is to compare a diverse range 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.

The challenge features three main tracks:

• Sequential Reachability: Verification/falsification of reachable source code labels (100 labels per problem)
• Sequential LTL: Verification/falsification of safety and liveness properties (100 LTL formulas per problem)
• Parallel LTL: Verification/falsification of safety and liveness properties (20 LTL formulas per problem)

Both sequential tracks are available in Java and C99 code. The Parallel LTL track is available as Promela code, Petri nets (PNML syntax), and a plain representation consisting of process graphs.

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, sequential and parallel problem description, and challenge rules pages. The evaluation thresholds and possible certificates are described on the rewards page.