Important Dates:

For Participants

Feedback

FAQ

Challenge Phase: starts 05.07.2013

The challenge phase of the RERS 2013 challenge has started! Below you find the 81 problems in defferent categories where each indiviual problems can be downloaded . Alternatively, a tarball for each section,containing all the problems, is also provided.

Problem Categories

As announced before, there will problems of three kind: 1) White-Box, 2) Black-Box and 3) Grey-Box ( problems replaced, new deadline 24.10.2013 ). Each of these categories will have 27 problems having different language features, size and difficulty levels. The details of the problem types are given bellow:

Problem Types:

Language feature: In terms of language feature there three types of problems – 1) plain 2) arithmetic and 3) array. The problems under the "plain" category include mere assignments over several basic types such as strings and integers. The problems under the "arithmetic" category additionally includes computation using integers and variables. Finally, the problems under the array category holds all the features of the “plain” and the “arithmetic” category and additionally includes operation on small arrays.

Difficulty level: On the basis of the degree of noise or obfuscation that has been put on top of the original code the difficulty levels of the problems have been assigned as easy, moderate, and hard. However, the behavior of the program has not been changed due to the obfuscation. The difficulty level “easy” means no obfuscation. In case of “moderate” and “hard” the size of the actual code has been artificially increased keeping the behavior indifferent, e.g., by inserting dead code.

Problem Description:

  • White-Box: there are three, behavioural and constructively indifferent, versions of each program. Two Java files, one with several variable types the other reduced to operating on integers, and a C file that also only operates on integers.
  • Grey-Box: an executable C file, and otherwise equal file setup to the White-Box problems, except that they contain black boxes. The files are not compilable. Additionally there are two test environment for each variable setup (mixed types or only integers) that serves as an oracle for the black box if the right system state is entered into the test environment.
  • Black-Box: an executable C file.

For each table there is one of 3 property files that describes the properties for all problems within the table. It contains the LTL formula that are to be checked additionally to the reachability of error states. Because of size limitations to java methods the body of the operating method has been split into many smaller parts. Inlining them into the operating method for analysis reasons is possible, but will make the compilation of the java files impossible.

Download Challenge Problems: