This collection of verification tasks is constructed and maintained as a common benchmark for evaluating the effectiveness and efficiency of state-of-the-art verification technology.
The verification tasks were contributed by several research and development groups. After the submission deadline of verification tasks for SV-COMP, a group of people (organizer and participants) are working on improving the quality of the verification tasks. This means that after the sets were made public, some programs were removed (not qualified, no property encoded, unknown architecture), and some programs got technically improved (CIL simplifications, compiler warnings, memory model). These changes have improved the overall quality of the final set of programs for the competition, and have not changed the intended verification result; all changes are tracked in the public repository.
Thanks to all contributors of programs, patches, and discussion commentes.
The collection consists of three directories, which contain verification tasks written in different languages:
- c/ (programing lagnuage C, follows the GNU C standard, many programs even adhere to ANSI C)
- java/ (programming language Java)
- causes/ (systems from the other directories translated to Horn clauses and stored in SMT format)
This repository is actively used by the competition on software verification SV-COMP, which is the reason why some of the text below is specific to SV-COMP.
The programs are accompanied by a license, either via a file LICENSE.txt in the same directory, or via a comment in the program header. The licenses must allow to:
- view, understand, investigate, reverse engineer the algorithm or system,
- change the program (in particular, pre-process and adopt the programs to be useful for a verification task),
- distribute the (original and changed) program (in particular, in replication packages for research projects or as regression tests),
- compile and execute the program (in particular, for the purpose of verifying that a specification violation exists), and
- commercially take advantage of the program.
The subdirectories that contain the programs contain files README.txt, which give further information about the programs, in particular, this is the place to trace the origin and to attribute the programs to their contributors. It is a good idea to link to project web sites and publications in those descriptions. For some programs, this information is given in the header of the program as comment.
The following definitions are taken from the SV-COMP report 2016 (and previous years).
A verification task consists of
- a program,
- a specification (set of properties), and
- parameters.
A category is a set of verification tasks.
A sub-category is a set of verification tasks that consist of the same specification and the same parameters. A sub-category is defined by the following three files:
- .set contains patterns that specify the set of programs,
- .prp contains the specification, and
- .cfg contains the parameters (and a description of the sub-category).
A verification run is
- a non-interactive execution
- of one verification tool
- on one verification task
- under specific resource constraints in order to check whether the following statement is correct: "The program satisfies the specification."
A verification result is a triple (ANSWER, WITNESS, TIME) with
- ANSWER is an element from {TRUE, FALSE, UNKNOWN},
- WITNESS is a violation witness or correctness witness that supports validation of the (untrusted) answer, and
- TIME is the CPU time that the verification run has consumed (in pratice, also other resource measurement values are reported).
A program file should be named as follows:
- the original file name or short title of the program is given at the beginning,
- for each property against which the program is to be verified,
the string
_false-<property>or_true-<property>is included, according to the expected verification answer, and - the filename ends with ending .c for not pre-processed files and .i for pre-processed files.
For example, the program minepump_spec5_product61_true-unreach-call_false-termination.cil.c
is expected to satisfy property unreach-call and to violate property termination.
There are some old programs that have ending .c although they are pre-processed.
This collection relies on contributions from many people. In order to contribute verification tasks, please use the following steps:
- fork the repository,
- commit your additions or changes to this repository,
- file a pull request, and
- discuss with community members until your contribution is approved and merged into the repository.
When pre-processing C files, please use the command cpp -P or something similar
that does not add line directives to the output.
Please make sure that you are pre-processing the files with the correct architecture
(e.g., on a 64-bit system, you need to specify -m32 for 32-bit programs)!
In order to be effectively used by people (e.g., in SV-COMP), the verification tasks need to be part of some category. Thus, please make sure that your programs are
- matched by the .set file,
- are made to be verified against the specification in the .prp file, and
- are compatible to the parameters in the .cfg file of the category.
For approving a pull request, it is a good idea to copy&paste the following checklist as comment to the pull request:
-
license present and acceptable (either in LICENCE.txt or as comment at beginning of program)
-
contributed-by present (either in README.txt or as comment at beginning of program
-
programs added to a .set file of an existing category, or new sub-category established (if justified)
-
intended property matches the corresponding .prp file
-
architecture (32 bit vs. 64 bit) matches the corresponding .cfg file
-
original sources present
-
preprocessed files present
-
preprocessed files generated with correct architecture
-
expected answer in file names according to convention
-
build system adjusted for enabling checks of this directory
-
build system can build the new benchmarks without warnings (both with gcc and clang)
For SV-COMP, the rules page explains all currently supported properties:
- unreach-call: A certain function call must not be reachable in the program.
- valid-memsafety, valid-deref, valid-free, valid-memtrack: A certain memory safety property must hold in the program. "memsafety" is the conjunction the other three properties.
- no-overflow: A certain kind of undefined behavior (overflows of signed ints) must not be present in the program.
- termination: The program must terminate on all execution paths.