Important Dates:

  • July 31th, 2022:
       Final submission, sequential
  • May 31st, 2022:
       Sequential problems
  • April 4th, 2022:
       Training problems

Sequential Problem Description

The Sequential Reachability and Sequential LTL tracks of the RERS Challenge 2022 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:

  1. conceptual complexity of the exhibited properties (reachability, safety, liveness),
  2. minimum/maximum counterexample depth for violated properties,
  3. 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
  4. language features (arrays, indirect addressing, floating point arithmetics, virtual method calls).

Reactive system

The problems are given in C99 code for which the detailed syntax is explained on an individual language page:

The generated C programs can output the statement "invalid input" in which case an error has occurred. In such a case, the valid execution of the system has ended after the "invalid input" statement. For convenience, instead of terminating, the program reverts back to the state prior to receiving the last input symbol before "invalid input" was outputted.

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 sequential track has its own set of properties to be analyzed. They are described in detail in the following paragraphs:

  • 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) 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 C99 code description.

    Each such __VERIFIER_error(int) defines a reachability problem, which you can solve with the method of your choice. There are no limitations.

  • LTL:

    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 file with behavioral LTL properties. This file defines the input and output alphabet in its first few lines. It contains a set of 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 C99 versions contain integers instead of specific input and output strings (an explicit request by participants). The corresponding mapping is specified in a file that is distributed with the given problem. If violating traces are provided, please convert them to the string format.

    Most of our LTL properties are accompanied by 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, sometimes just W): φ 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.

    These 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,....