The background color is gold for the winner,
silver for the second, and bronze for the third.
Here some brief directions for reading the score-based quantile plots:
The right end of the graph displays the achieved score. The score is SV-COMP's definition of quality.
You can read the ranking on the top from right to left.
The left end of the graph displays the amount of wrong results that a verifier produced. Left-most start means worst.
The length of the graph displays the amount of correct verification work. Long is good.
More about what you can learn from a score-based quantile plot and how to interpret it,
is described in the SV-COMP 2015 report,
on pages 12 and 13.
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 2022 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".
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.
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).
Competition Report of SV-COMP 2023