Updates

  • 10/04/15 Results up
  • 10/02/15 Solutions for challenge up
  • 09/05/15 RV traces and ext. file released
  • 08/26/15 Submission opened, RV dates updated
  • 07/18/15 RV training traces
  • 05/15/15 Training solutions up

Important Dates:

  • 05/15/15
       Solutions Training Phase
  • 08/01/15 - 09/04/15
       White Box Submission
  • 09/05/15
       Release Monitoring Input
  • 09/08/15
       RV Submission

Challenge Setup and Rules

This year’s challenge will consist of 6 problems, divided into 2 categories. The problems will range from structurally simple and small to structurally complex and huge. More detailed information about the exact generation process and syntax of the problems can be found on the problem description page. This years categories are:

  • White-Box: this are programs syntactically in the same fashion as for the RERS 2014 challenge. The source code is provided in Java and C.
  • RV Monitoring: these are generated in the same fashion as the White-Box problems (in Java and C), but additionally have calls to an external file with unknown code.

The corresponding collections of properties to be checked against these systems fall into two categories:

  1. implicit ones, given by errors/exceptions/assertions. These properties are only implicitly given within the code and should be checked for reachability. Each individual reachability problem is evaluated and ranked exactly in the same fashion as the explicit properties. There are 100 overall properties for each problem.
  2. explicit ones, described verbally and formalized in temporal logic (LTL, the exact syntax is given on this page).

For each White Box problem there are 100 LTL formulae and 100 reachability properties to be answered. For each RV Monitoring problems there are 100 LTL formulae to be answered. For successfully answering of questions there will be rewards and achievements for which further information can be found on this page.

White Box Problems

For each problem there are 3 files provided. The C source code file (ProblemX.c), the Java source code file (ProblemX.java) and a constraints file containing 100 LTL properties. A detailed description of the code layout can be found on the this page. There are no constraints on the application of methods, so participants can modify the source code in any way imaginable. In particular participants are not constrained to their own tools. It is not required to submit the code that produced the challenge results. Only the "yes" and "no" answers in the submitted solutions are considered for the ranking and achievements. For winning an evaluation-based award it is however required to describe the approach for computing the solutions.

Runtime Verification: Monitoring

The monitoring problems are generated in the same fashion as the White-Box problems (in Java and C), but additionally the usual problem file (ProblemX) contains calls to an external file (ProblemXExternal) with modified/not trustable source code. The participants have to instrument/parameterize the ProblemX code file so events are triggered according to conditions resulting from the stdin, the stdout, and the code in the external file. For the evaluation phase, which will last for a short period of time at the beginning of September, a set of input sequences will be provided along with a new ProblemXExternal file. The participants will have to report the results that are expected when executing the inputs on the system. It is guaranteed that all unsatisfied LTL properties will be violated on one of the provided paths.

It is not required to provide the monitor code or running times of the monitoring process. The submit page gives detailed information about how the solutions have to be submitted.