The RERS Challenge 2014 will provide a wealth of benchmark problems of increasing complexity, the more involved of which will probably be beyond any individual state-of-the-art method or tool. A large set of benchmarks will be synthesized to exhibit chosen properties, and then enhanced in an automated process to cover dedicated dimensions of difficulty, including:

1. conceptual complexity of the exhibited properties (reachability, safety, liveness),
2. size of the systems in lines of code (from a few hundred lines to thousands of them) and size in terms of the state space to be explored, and
3. language features (arrays, indirect addressing, floating point arithmetics, virtual method calls, recursion).

The problems are given in Java, C or Promela code for which the detailed syntax is explained on individual language pages:

• Java code syntax description
• C code syntax description

The challenge rules are essentially free style in order include as many participants as possible. Details on the generation process of the Java and C problems can be found in this paper.

Properties to analyze

For each of the systems, the contestants have to answer several questions, which can be divided into two classes:

• Reachability:

  Some assignments to internal state variables correspond to erroneous states, which cause the system to fail with a specific error code. Not all of those error states are reachable, and the goal is to check which of these states can in fact be reached (it is not expected to also provide a sequence of inputs reaching them). Those errors come in the form of either an uncaught IllegalStateException in Java or failed assertion in C which both terminate the program. The IllegalStateException comes with a specific error label that can be extracted from the exception. In C there is an error label followed by assert, which prints the error label on the error stream.

  Each error/exception/assertion label defines a reachability problem, which you can solve with the method of your choice. There are no limitations.

• Behavioral properties:

  An execution trace of a challenge system consists of a sequence of inputs and outputs, each from a finite alphabet. There exist 4 files with behavioral properties, each of which is designed for a specific input alphabet size. The input alphabet size also determines for which systems the respective file applies. They contain a set of 100 properties for which the contestants have to check whether they are satisfied by all traces, or if there are traces that violate them (it is not expected to also provide these traces). The alphabet sizes in this challenge are of the sizes 5, 10, 15 and 20 input symbols.

  Some problems are provided with plain numbers as input and output symbols instead of strings which are used to specify the LTL formulae (an explicit request from participants). The translation is intuitive: "A" is 1, "B" is 2 etc. If violating traces are provided, please convert them to the string format.

  The properties are given both as an LTL formula and a textual description. For example,

      (G ! oU)
      output U does never occur
  

  states that it is not possible — by any sequence of input events — to make the system produce an "U" output action.

  In the LTL formulae, the atomic propositions correspond to input and output symbols, where the prefix i is used for input and o is used for output symbols, to allow a clear distinction.

  The LTL formulae are given in a standard syntax, making use of the following temporal operators:

  • X φ (next): φ has to hold after the next step
  • F φ (eventually): φ has to hold at some point in the future (or now)
  • G φ (globally): φ has to hold always (including now)
  • φ U ψ (until): φ has to hold until ψ holds (which eventually occurs)
  • φ WU ψ (weak until): φ has to hold until ψ holds (which does not necessarily occur)
  • φ R ψ (release): φ has to hold until ψ held in the previous step.

  Additionally, the boolean operators & (conjunction), | (disjunction) and ! (negation) are used.

  This properties, even if reminding of typical model checking problems, may also be dealt with in any fashion you like, e.g. data-flow analysis, symbolic execution, testing, learning, (statistical) model checking, run-time methods,....

Formal behavioral semantics

For evaluating the LTL formulae on the challenge problems, it is important to formally understand the behavioral semantics of the programs.

A program reads inputs (events) from the command line, and upon each event emit an output (for simplicity we restrict this to a finite set of outputs, of which at most one is issued before the next event occurs). Hence, an (infinite) run is an infinite word over a sequence of input and output symbols. The validity of an LTL formula over such a word is straightforward.

The LTL properties are intended to only specify the error-free behavior of the system. The rationale behind this is that it allows to formulate the specifications in a more compact way. For example, specifying that event A eventually leads to output Z being generated and interpreting it to hold for non-error runs only is probably more intuitive than specifying that A eventually leads to either Z or a fatal error.

Summing this up, an LTL property holds for a certain program if and only if all possible runs which do not lead to an error satisfy the LTL property. Additionally, the LTL formulae are only defined for the specified alphabet, inputs that are not in the alphabet are ignored by the program (no change of the internal state) and should not be considered for the evaluation of LTL properties.