Benchmark Verification Tasks

All verification tasks are available for web browsing and for download via the following Git repository: (for SV-COMP 2025 visit the tag 'svcomp25'): https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks

This edition of the competition on software verification is based on the following categories of verification tasks. The verification tasks were contributed by several research and development groups. After the submission deadline for verification tasks, a group of people (organizer and participants) were working on improving the quality of the verification tasks. That 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 participants who contributed programs, sent patches, and commented on the sets.

As announced in the rules and definitions, the verification tasks are not necessarily preprocessed with CIL (which was a restriction for the first SV-COMP). For each verification task, we specify whether it assume a 32-bit or a 64-bit architecture.

For illustration, a structured overview (2025) shows the categories below. Rankings will be provided for the first- and second-level categories, and FalsificationOverall, which is not shown in the figure.

The authorative definition of the category structure (from which this web page is generated) is maintained in the repository for the benchmark definitions (https://gitlab.com/sosy-lab/sv-comp/bench-defs).

1. C.ReachSafety

unreach-call

The verification tasks consist of the programs that match

with the specification:


  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    



2. C.MemSafety

  
 valid-memcleanup

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 valid-memsafety

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 valid-memsafety

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 valid-memsafety

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 valid-memsafety

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 valid-memsafety

    
The verification tasks consist of the programs that match

    
with the specification:

    



3. C.Concurrency

  
 no-data-race

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 no-overflow

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 valid-memsafety

    
The verification tasks consist of the programs that match

    
with the specification:

    



4. C.NoOverflows

  
 no-overflow

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 no-overflow

    
The verification tasks consist of the programs that match

    
with the specification:

    



5. C.Termination

  
 termination

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 termination

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 termination

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 termination

    
The verification tasks consist of the programs that match

    
with the specification:

    



6. C.SoftwareSystems


This category consists of several sets of verification tasks. Each of these sets is an own sub-category.
While the categories above are collections of rather `academic', or synthesized, example verification tasks,
this category aims to represent verification tasks from real software systems.


  
 no-overflow

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 no-overflow

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 no-overflow

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 termination

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 valid-memcleanup

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 valid-memsafety

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 valid-memsafety

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 valid-memsafety

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 valid-memsafety

    
The verification tasks consist of the programs that match

    
with the specification:

    



7. C.ValidationCrafted


This category contains validation tasks that were crafted to test certain features of validators.


  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 termination

    
The verification tasks consist of the programs that match

    
with the specification:

    



8. C.Overall


The category C.Overall contains all verification tasks of all above categories.
Each above-mentioned main category is an own sub-category in category C.Overall.
(The weighting schema is explained on the rules page.)


  
 ReachSafety

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 MemSafety

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 Concurrency

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 NoOverflows

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 Termination

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 SoftwareSystems

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 ValidationCrafted

    
The verification tasks consist of the programs that match

    
with the specification:

    



9. C.FalseOverall


The category C.FalseOverall consists of all verification tasks
and the results "correct TRUE" and "incorrect TRUE" are not counted.
(The weighting schema is the same as for C.Overall.)


  
 ReachSafety

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 MemSafety

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 Concurrency

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 NoOverflows

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 Termination

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 SoftwareSystems

    
The verification tasks consist of the programs that match

    
with the specification:

    



10. C.TrueOverall


The category C.TrueOverall consists of all verification tasks
and the results "correct FALSE" and "incorrect FALSE" are not counted.
(The weighting schema is the same as for C.Overall.)


  
 ReachSafety

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 MemSafety

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 Concurrency

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 NoOverflows

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 Termination

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 SoftwareSystems

    
The verification tasks consist of the programs that match

    
with the specification:

    



11. C.Huawei-Concurrency-Challenges

  
 no-data-race

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 no-overflow

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 unreach-call

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 valid-memsafety

    
The verification tasks consist of the programs that match

    
with the specification:

    



12. Java.Overall

  
 no-runtime-exception

    
The verification tasks consist of the programs that match

    
with the specification:

    

  
 valid-assert

    
The verification tasks consist of the programs that match

    
with the specification: