Demonstration Categories (without Rankings)

All verification tasks are available for web browsing and for checkout via the following SVN repository: https://svn.sosy-lab.org/software/sv-benchmarks/trunk/c

A. Stateful Verification

The verification tasks in the category Stateful collect similar programs for which it should be beneficial to reuse some (intermediate) verification results (or artifacts) from previous verification runs:


The verifiers are allowed to write state information into a directory that is passed as parameter to the verifier. The verifier can store any information about previous runs, and can unrestrictedly read from the state information. The parameter is speficied in the system description of the verifier.
The verification tasks were taken from the supplementary web page of the paper on Precision Reuse.
Description: regression

Memory Model: Simple
Architecture: 64 bit

B. Error-Witness Checking

This category consists of verification tasks for which the result is FALSE (more specifically, false-unreach-label). In a first round, the produced error witnesses need to be readable for (re-) verification by the verifier. In a second round, the verifier gets as input a verification task (program and property) and an error witness from a different verifier, and is supposed to check if the error witness corresponds to a feasible error path in the given program and violates the given property.

Note that if an error witness is given as input, the result of the verification task should be FALSE if the verifier can find a feasible error path that is represented by the error witness. If the verifier cannot find a feasible error path from the guidance by the error witness, then the correct result of the verifier is TRUE (the program satisfies the specification along all paths that the error witness represents).

The error-path format to be used (at least in B2) is still in beta version and will be further improved; suggestions welcome.

C. Device-Driver Challenges

This category consists of verification tasks for which no confirmed results are given.


The problems in this category were contributed by the Linux Driver Verification project.
Description: ldv

Memory Model: Simple
Architecture: 64 bit

D. Termination

This category consists of verification tasks for which the verifier has to prove termination. The property file contains
CHECK( init(main()), LTL(F end) )
and means that each path that starts by calling function "main" finally reaches the end of the program. The proposition "end" is true at the end of every finite program execution (return of main, exit, abort, etc.). A counterexample for this property is an infinite program execution. (This is a liveness property, and thus, counterexamples must have maximal execution length, i.e., are terminating or infinite; all terminating paths end with proposition "end".)

For the result "FALSE + Error Path", the error path has to be a finite path from to the entry of a non-terminating loop. In addition, a second path may be appended that leads from the entry of the non-terminating loop back to the entry of this loop and corresponds to an infinite execution.

This category consists of two subcategories.

The first subcategory contains the following verification tasks, for which the result is already known:


The verification tasks in this category were contributed by the Ultimate team.
Description: termination

Memory Model: Simple
Architecture: 64 bit

The second subcategory contains the following verification tasks, for which the result is not yet known:



Memory Model: Simple
Architecture: 32 bit