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.
This repository is used by many research groups to evaluate the effectiveness and efficiency of verification algorithms for software. The category structure was developed for the International Competition on Software Verification SV-COMP.
The verification tasks were contributed by several research and development groups. After the submission of verification tasks, a group of people (mainly SV-COMP 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 (no property encoded, unknown architecture), and some programs got technically improved (compiler warnings, memory model). These changes have improved the overall quality of the final set of programs for the competition SV-COMP, and have not changed the intended verification result; all changes are tracked in the public repository.
This repository is open for submission of new verification tasks! Please refer to our contribution guidelines to see how to submit verification tasks to this repository.
Thanks to all contributors of programs, patches, and discussion comments.
The collection consists of three directories, which contain verification tasks written in different languages:
c/ (programming language 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)The programs are under different licenses, which are specified either via a file LICENSE*.txt in the same directory,
or via a comment in the program header.
Most of the programs are under an open-source license such as Apache 2.0 or GPL.
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.
For some programs, this information is given in the header of the program as comment.
The verification tasks for C programs are grouped into (sub-)categories as defined by SV-COMP.
A (sub-)category <category> is defined by a file named <category>.set
that contains patterns that specify the set of programs.
The following definitions are taken from the SV-COMP report 2016 (and previous years).
A verification task consists of
A category is a set of verification tasks.
A sub-category is a set of verification tasks that consist of the same specification.
A verification run is
A verification result is a triple (ANSWER, WITNESS, TIME) with
The program files in this repository are named as follows:
_false-<property> or _true-<property> is included, according to the expected verification answer, and.c for not preprocessed files and .i for preprocessed files (for C 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 preprocessed.
There are several 'default' specifications that many people use:
The above specifications are used, e.g., by SV-COMP, and the competition reports explains those specifications.
The following are some 'default' specifications that many people use for test-case generation:
The above test specifications are used, e.g., by Test-Comp, and the competition reports define those specifications.
The parameters of a verification task are needed to make additional information about the verification task available to the verification run. The most prominent parameter is the machine model; currently, there are verification tasks for the ILP32 (32-bit) and the LP64 (64-bit) architecture (cf. https://www.unix.org/whitepapers/64bit.html).
In order to obtain verification tasks from the programs and specifications in the repository, a simple task-definition mechanism is used. We use version 2.0 of this format with some additional requirements. For each program, the repository contains a .yml file that specifies the following items:
format_version: the version of the format (the version string 2.0)input_files: the subject program files or directories
(a file or directory name, or a list of files or directory names, that the program consists of)properties: the properties that constitute the specification of the program,
each consisting of the following items:
property_file: file that contains a property definition
(cf. common property files for C and for Java)expected_verdict: the intended verification result (true or false, only for non-coverage properties)subproperty (optional): a subproperty of the property that is violated
in cases where the property is a conjunction of subproperties (for verdict false)options: parameters that are relevant for verification or give extra information:
language: programming language that the program is written in (C or Java)data_model data model of the computer architecture
(ILP32, LP64, see https://www.unix.org/whitepapers/64bit.html, only for C programs)Optional items are explicitly marked as optional, all other items are mandatory.
The dictionary options can contain additional data that are not mentioned above.
The SV-COMP 2019 report has documented the first version of the repository's task-definition format 1.0,
and contains a description of the format with an example in Sect. 4 and Fig. 3.
Format 2.0 adds the options dictionary.
Here as example an extract of the task-definition file c/list-properties/list-1.yml:
format_version: '2.0'
input_files: 'list-1.i'
properties:
- property_file: ../properties/unreach-call.prp
expected_verdict: true
- property_file: ../properties/valid-memsafety.prp
expected_verdict: false
subproperty: valid-memtrack
options:
language: C
data_model: ILP32