TACAS 2024
13th Competition on Software Verification (SV-COMP 2024)

Results of the Competition on Witness Validation

This web page presents the results of SV-COMP 2024 - 13th International Competition on Software Verification.

• Proposal of Validation Track and Scoring Schema (Proc. SAS 2022)
• The benchmarks and rules are also available from the competition web site.

The background color is gold for the winner, silver for the second, and bronze for the third.

Here some brief directions for navigating in the BenchExec-generated tables with the results:

• Please note the header with the menu "Select Columns, Filter Rows, etc.", which loads only after all data are retrieved from the server.
• The tables contain all information that I thought you could be interested in. If there are too many columns, you can get rid of some with "Select Columns". You can also investigate special classes of rows using "Filter Rows".
• If you want to see more data, including the time and memory needed for witness validation, please click on the score value in a table cell (works only for base categories). In those tables, there is also a link available to get the witness that the verifier generated.
• In all results tables, the sources of the verification task is available via click on the name of the verification task. The log files are available via click on the status (result).
• If you want to investigate even more, you can download the SV-COMP 2024 results archive, which contains all data that I obtained with BenchExec and from which I compiled all the tables and aggregated data displays. For the most detailed tables, which end on ".xml.bz2.table.html", you can obtain the raw data by accessing the URL with the ".table.html" removed.
• Falsification: Here only bug hunting matters and proof generation is ignored. There are no different results tables for the Falsification category because all verification tasks (except Termination) are included, but the TRUE results are ignored (no score assigned). If you want to remove for a particular verifier the TRUE results, proceed as follows: Click in the menu on "Filter Rows". Then select "status" for the verifier you are interested in for row selection, then a choose box with all the status-values appears. There you choose "true" and then click "invert filter".
• More on table generation is described here.
• Column "score" shows the (not normalized) score assigned to the result of the verification task.
• Column "witness" contains a link to the witness file for download/display.
• Column "inspect witness" opens a new page that displays information about the witness an a list of witnesses that other verifiers produced for the same program.
• Column "cpu" shows the consumed CPU time.
• Column "wall" shows the elapsed wall time.
• Column "energy" shows the energy consumed by the CPU.
• Column "mem" shows the peak memory usage.
• Column "blkio-w" shows the accumulated amount of information written to block devices.
• Column "blkio-r" shows the accumulated amount of information read from block devices.
• More information on results.

Contents

1. Validation of Correctness Witnesses (Version 2.0)
2. Validation of Violation Witnesses (Version 2.0)
3. Validation of Correctness Witnesses (Version 1.0)
4. Validation of Violation Witnesses (Version 1.0)

1. Validation of Correctness Witnesses (Version 2.0)

Ranking by Category (with Score-Based Quantile Plots)

Table of All Results

In every table cell for competition results, we list the points in the first row and the CPU time (rounded to two significant digits) for successful runs in the second row.

The entry '–' means that the competition candidate was not executed in the category.
The definition of the scoring schema can be found in the literature [Proc. SAS 2022] and the categories are defined on the respective SV-COMP web page.

Hide base categories

2. Validation of Violation Witnesses (Version 2.0)

Ranking by Category (with Score-Based Quantile Plots)

Validation of violation witnesses was a demonstration category in SV-COMP 2024.

Table of All Results

In every table cell for competition results, we list the points in the first row and the CPU time (rounded to two significant digits) for successful runs in the second row.

The entry '–' means that the competition candidate was not executed in the category.
The definition of the scoring schema can be found in the literature [Proc. SAS 2022] and the categories are defined on the respective SV-COMP web page.

Hide base categories

3. Validation of Correctness Witnesses (Version 1.0)

Ranking by Category (with Score-Based Quantile Plots)

Table of All Results

In every table cell for competition results, we list the points in the first row and the CPU time (rounded to two significant digits) for successful runs in the second row.

The entry '–' means that the competition candidate was not executed in the category.
The definition of the scoring schema can be found in the literature [Proc. SAS 2022] and the categories are defined on the respective SV-COMP web page.

Hide base categories

4. Validation of Violation Witnesses (Version 1.0)

Ranking by Category (with Score-Based Quantile Plots)

Table of All Results

In every table cell for competition results, we list the points in the first row and the CPU time (rounded to two significant digits) for successful runs in the second row.

The entry '–' means that the competition candidate was not executed in the category.
The definition of the scoring schema can be found in the literature [Proc. SAS 2022] and the categories are defined on the respective SV-COMP web page.

Hide base categories

Note on meta-categories: The score is not the sum of scores of the sub-categories (normalization). The run time is the sum of run times of the sub-categories, rounded to two significant digits.

If you did not find what you are looking for, please do not hesitate to contact Dirk Beyer (competition chair).