Sequential Problem Description
The RERS Challenge 2016 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. The benchmarks are synthesized to exhibit chosen properties, and then enhanced in an automated process to cover dedicated dimensions of difficulty, including:
- conceptual complexity of the exhibited properties (reachability, safety, liveness),
- 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
- language features (arrays, indirect addressing, floating point arithmetics, virtual method calls).
The problems are given in Java or C99 code for which the detailed syntax is explained on individual language pages:
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
Each category has its own set of properties to be analyzed. They are described in detail in the following passages:
- Reachability:
These properties are relevant for the Reachability problems. 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). The error are model in form of an external undefined function __VERIFIER_error(int) (Errors.__VERIFIER_error(int) for Java) whose semantic abruptly terminates the program. The passed integer refers to the number of the error that caused the termination. If you want to compile and execute the problems please check the Java and C99code syntax description.
Each error/exception/assertion label defines a reachability problem, which you can solve with the method of your choice. There are no limitations.
- Semantic of behavioral properties:
These properties are relevant for the LTL problems. An execution trace of a challenge system consists of a sequence of inputs and outputs, each from a finite alphabet. The input and output symbols alternate, i.e., the output produced in response to an input occurs at the point in time immediately succeeding the time of the input event.
For example, given the formula (i U o3), the trace i, o1, i, o2, i, o3 does not satisfy the formula as i does not hold in the second step.
For each problem there exists a files with behavioral properties that defines the input and output alphabet at the top of the constraints file. It contains 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).
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,....