Proposal for LTL demo category in SVCOMP 17

[danieldietsch]

In the (Demo)Category, we check whether C programs satisfy LTL properties.

Each verification task consists of a C program and a .prp property file. Each .prp files corresponds to one program, the program filename is prefix of prp file. For each program there can be several .prp files. The verdict (_true-??? or _false-???) of each verification task is encoded in the filename of the .prp file.

The initial proposal for an LTL demo category was sent to the SVCOMP list as follows.

Hi All, Matthias Heizmann and I would like to present a proposal for a new SV-COMP category: temporal property verification. It seems there are now numerous tools that are able to verify both safety and liveness properties for C programs. We would therefore like to have a category were such tools can compete.

Basically, a verification task would consist of a C program and one temporal property; the following rules should apply for this category

• Properties are LTL properties without the Next-operator using a subset of the Spot [1] syntax, i.e., temporal formulas of the form \phi := "P" | \phi || \phi | \phi && \phi | !\phi | G \phi | F \phi | \phi U \phi | \phi W \phi | \phi R \phi where \phi is a temporal formula and "P" is an atomic proposition.
• Atomic propositions are Boolean, side-effect free expressions over the global program variables, i.e., side-effect Boolean C expressions that only contain global variables.
• Atomic propositions must not contain function calls.
• A temporal property has to hold after the initialization of all global variables, i.e., before the first transition of the entry method of the C program.
• If the evaluation of an atomic proposition may lead to undefined behavior (i.e., array access, pointer dereferences, pointer arithmetic, overflows, etc.), the C file must guarantee that this cannot happen, i.e., the evaluation of an atomic proposition may not lead to undefined behavior.
• A single property is specified in a separate file named <input-filename>-<property-id>.ltl
• We currently do not support witnesses (violation or otherwise) and thus do not require them.

Team Ultimate will prepare an initial set of verification tasks based on the benchmark suites used in [2].

Best, Daniel

[1] https://spot.lrde.epita.fr/tl.pdf [2] Dietsch, D., Heizmann, M., Langenfeld, V., & Podelski, A. Fairness modulo theory: A new approach
to LTL software model checking. In CAV 2015.

We should create an updated proposal here that contains all the issues that were raised in the past.

[danieldietsch]

Ok, here is a new proposal:

Hi All, Matthias Heizmann, Vincent Langenfeld and I would like to renew our proposal for an LTL property verification category. We would like to add this category as demo category to SV-COMP'17 and have a run before we meet in Uppsala at the end of April.

The following rules should apply for this category

• Properties are LTL properties without the Next-operator using the following syntax. \phi := "P" | \phi || \phi | \phi && \phi | !\phi | G \phi | F \phi | \phi U \phi | \phi W \phi | \phi R \phi where \phi is a temporal formula and "P" is an atomic proposition.
• A verification task consists of a C program and one temporal property. The temporal property is specified in a .prp file as check-clause, e.g. "CHECK( init(main()), LTL(\phi) )".
• A temporal property has to hold after the initialization of all global variables, i.e., before the first transition of the entry method of the C program. The entry method is specified by the init() clause of the check clause.
• Atomic propositions are Boolean, side-effect free expressions over the global program variables, i.e., side-effect Boolean C expressions that only contain global variables.
• Atomic propositions must not contain function calls.
• If the evaluation of an atomic proposition may lead to undefined behavior (i.e., array access, pointer dereferences, pointer arithmetic, overflows, etc.), the C file must guarantee that this cannot happen, i.e., the evaluation of an atomic proposition may not lead to undefined behavior.
• We currently do not support witnesses (violation or otherwise) and thus do not require them.
• The scoring scheme is as usual (2 for safe, 1 for unsafe, -16 for incorrect unsafe, -32 for incorrect safe)
• Results should be reported as TRUE if the program fulfills the LTL property or as "false(valid-ltl)" if the program violates the LTL property.
• The expected result is encoded in the filename as well as in the property filename as true-valid-ltl and false-valid-ltl.
• .prp filenames are .prp, e.g. some-task-true-valid-ltl.c and some-task-true-valid-ltl.c.prp

Team Ultimate has already prepared an initial set of verification tasks (cf. pull request ...) and modified benchexec (cf. pull request #234) such that the category can take place.

Best, Daniel

[Heizmann]

Revised version. Changes: merged bullets, tried to use SV-COMP terminology, emphasize that we only extend existing formalisms.

Hi All, Matthias Heizmann, Vincent Langenfeld and I would like to renew our proposal for an LTL property verification category. We would like to add this category as demo category to SV-COMP'17 and have a run before we meet in Uppsala at the end of April.

The following rules should apply for this category

1. Each verification task consists of a C program and one temporal property. The temporal property is specified in a .prp file as check-clause of the form "CHECK( init(main()), LTL(\phi) )", where \phi is an LTL formula. The string init(main()) refers to the set of states in which the program can be directly after the main function was called without arguments. We note that e.g., global variables have been initialized at this point (see §5.1.2 of the C99 standard). Verifiers have to check whether the LTL formula \phi holds in each init(main()) state.
2. We use only the fragment of LTL properties that can be defined without the "next" operator. We use the following subset of the Spot [1] tool's syntax \phi := "P" | \phi || \phi | \phi && \phi | !\phi | G \phi | F \phi | \phi U \phi | \phi W \phi | \phi R \phi where \phi is a temporal formula and "P" is an atomic proposition.
3. Atomic propositions are Boolean, side-effect free expressions that neither contain local variables nor function calls.
4. If the evaluation of an atomic proposition may lead to undefined behavior (i.e., array access, pointer dereferences, pointer arithmetic, overflows, etc.), the C file must guarantee that this cannot happen, i.e., the evaluation of an atomic proposition may not lead to undefined behavior.
5. We use the strings true-valid-ltl and false-valid-ltl to encode the expected results of a verification task. The expected result is encoded in the program filename as well as in the property filename.
6. The name of the property file is the name of the C program appended by ".prp".
7. The verifier should return "TRUE" if the LTL property holds and "false(valid-ltl)" otherwise.
8. This year, tools neither have to provide violation witnesses nor correctness witnesses.
9. The scoring scheme is as usual (2 for safe, 1 for unsafe, -16 for incorrect unsafe, -32 for incorrect safe)

Additional comments

• We do not support the "next" operator because yet we do not want to define what one step of a C program is.
• We do not support local variables in LTL formulas because yet we do not yet want to define whether e.g. the expression x==0 is valid in a scope where x does not occur.

Team Ultimate has already prepared an initial set of verification tasks (cf. pull request ...) and modified benchexec (cf. pull request #234) such that the category can take place.

Best, Daniel

[danieldietsch]

Looks good except two things:

• The reference to SPOT was removed to make the definition self-contained (I think Dirk requested this). We can rephrase this as a note or comment if you want to keep it.
• init() is already part of the CHECK clause in SV-COMP. I would also rephrase the bullet (1) somewhat:

  The string init(main()) refers to the set of states in which the program can be directly after the main function was called without arguments.

The string init() refers to the set of states in which the program can be directly after the function was called. Usually, is ´main()´, i.e., a call without arguments to the entry function of the program.

Verifiers have to check whether the LTL formula \phi holds in each init(main()) state.

Verifiers have to check whether the LTL formula \phi holds starting in each init(main()) state.

[Heizmann]

1. The definition is self-contained. Dirk was afraid that we only refer to SPOT but do not show the syntax.
2. At the moment we use only main()

[danieldietsch]

Regarding SPOT: Dirks quote was

1. Is the reference to Spot required? It is bad to have the definition not self-contained. If it is only about omitting X, then the user does not need to read about Spot. Everything seems standard and not Spot-specific at all.

I propose the following change.

We use only the fragment of LTL properties that can be defined without the "next" operator. We use the following subset of the Spot [1] tool's syntax \phi := "P" | \phi || \phi | \phi && \phi | !\phi | G \phi | F \phi | \phi U \phi | \phi W \phi | \phi R \phi where \phi is a temporal formula and "P" is an atomic proposition.

We use only the fragment of LTL properties that can be defined without the "next" operator. We use the following syntax. \phi := "P" | \phi || \phi | \phi && \phi | !\phi | G \phi | F \phi | \phi U \phi | \phi W \phi | \phi R \phi where \phi is a temporal formula and "P" is an atomic proposition. Note that this is a subset of the Spot [1] tool's syntax.

Regarding main(): We already support arbitrary entry functions. I want to avoid confusion between "main function" and "main()".

[danieldietsch]

Latest version for reference (cf. mail)

Hi All, Matthias Heizmann, Vincent Langenfeld and I would like to renew our proposal for an LTL property verification category. We would like to add this category as demo category to SV-COMP'17 and have a run before we meet in Uppsala at the end of April.

The following rules should apply for this category

1. Each verification task consists of a C program and one temporal property. The temporal property is specified in a .prp file as check-clause of the form CHECK( init(main()), LTL(\phi) ), where \phi is an LTL formula. The string init() refers to the set of states in which the program can be directly after the function was called. Usually, is main(), i.e., a call without arguments to the entry function of the program. We note that e.g., global variables have been initialized at this point (see §5.1.2 of the C99 standard). Verifiers have to check whether the LTL formula \phi holds starting in each init(main()) state.
2. We use only the fragment of LTL properties that can be defined without the "next" operator. We use the following syntax. \phi := "P" | \phi || \phi | \phi && \phi | !\phi | G \phi | F \phi | \phi U \phi | \phi W \phi | \phi R \phi where \phi is a temporal formula and "P" is an atomic proposition. Note that this syntax is a subset of the Spot [1] tool's syntax.
3. Atomic propositions are Boolean, side-effect free expressions that neither contain local variables nor function calls.
4. If the evaluation of an atomic proposition may lead to undefined behavior (i.e., array access, pointer dereferences, pointer arithmetic, overflows, etc.), the C file must guarantee that this cannot happen, i.e., the evaluation of an atomic proposition may not lead to undefined behavior.
5. We use the strings true-valid-ltl and false-valid-ltl to encode the expected results of a verification task. The expected result is encoded in the program filename as well as in the property filename.
6. The name of the property file is the name of the C program appended by ".prp".
7. The verifier should return "TRUE" if the LTL property holds and "false(valid-ltl)" otherwise.
8. This year, tools neither have to provide violation witnesses nor correctness witnesses.
9. The scoring scheme is as usual (2 for safe, 1 for unsafe, -16 for incorrect unsafe, -32 for incorrect safe)

Additional comments

• We do not support the "next" operator because yet we do not want to define what one step of a C program is.
• We do not support local variables in LTL formulas because yet we do not yet want to define whether e.g. the expression x==0 is valid in a scope where x does not occur.

Team Ultimate has already prepared an initial set of verification tasks (cf. pull request ...) and modified benchexec (cf. pull request #234) such that the category can take place.

Best, Daniel

[1] https://spot.lrde.epita.fr/tl.pdf