DOI: 10.5281/zenodo.17371298
title: Artifact: Visualization of Verification Results for Linux Kernel Benchmarks with CV

description: This artifact accompanies Continuous Verification (CV) -- a framework for visualizing software verification results with support for regression verification. It includes:



Visualized verification results

Benchmarks

Docker image

Error trace visualization for SV-COMP tools

Correctness proofs visualization for SV-COMP tools


A short video demonstration can be found here: https://youtu.be/98JzOwgKmjY.

CV framework repository is: https://github.com/ispras/cv.

Web-interface repository is: https://github.com/ispras/cv-visualizer.

1. Visualized Verification Results

Pre-generated visualization datasets are provided for three verification properties and three Linux kernel versions:





Properties:





Memory Safety




Concurrency Safety




Clock API






Kernel Versions:





5.10.227




5.10.231




5.10.235





Each visualization dataset is packaged as:

result_<property>_<version>.zip


To explore results, deploy the CV Web Interface and upload archives through the interface.

2. Benchmarks

This artifact provides the complete benchmark set used in the evaluation. Benchmarks consist of Linux kernel modules ('net' and `usb` drivers) prepared using Klever.

For each of the three properties and three kernel versions, a benchmark archive is provided in the format:

benchmark_<property>_<version>.zip


Each archive includes:





Preprocessed C files (via CIL) with an injected main() entry point.




Encoded property for the corresponding verification tasks.



The benchmarks can be executed with any SV-COMP compatible verification tool.

3. Docker Image

This artifact provides a ready-to-run Docker image containing all visualized benchmark results and user marks.

How to install it:

1. Load the Docker image

Download the file cv-image.tar and load it into Docker:

docker load -i cv-image.tar


2. Run the container

Start the container and expose the web interface on port 8989:

docker run -it -p 8989:8989 --name cv-artifact cv-artifact:v3


The startup may take up to 1 minute.Once initialization is complete, you will see:

Starting CVV Web Interface...


3. Access the Web Interface

Open a browser on the host machine and navigate to:

http://<your-machine-ip>:8989


Log in using the default credentials (admin/admin). You can later change them in the Settings panel.After logging in, the main page displays grouped benchmark results.From there, you can explore individual benchmarks, including error traces and correctness proofs.

For additional details and usage instructions, please refer to the project repository.

4. Stop and remove the container

When finished, stop the container and clean up:

docker stop cv-artifact
docker rm cv-artifact
docker rmi cv-artifact:v3

4. Error Trace Visualizations for SV-COMP Tools

This dataset provides a single representative none-empty error trace for each SV-COMP’2025 C verification tool, along with its visualization generated by CV in a stand-alone mode. A summary of the presence of key elements across tools is provided in the corresponding evaluation table.

Table. 1. Evaluation of error traces for all SV-COMP’2025 tools.




SV-COMP Tool
Function calls
Thread information
Assumptions
Conditions
Loop heads
Violation hints




2LS
-
-
+
-
-
-


AISE
-
-
+
-
-
-


AProVE
-
-
-
+
+
-


BRICK
-
-
+
-
-
-


Bubaak
-
-
+
-
-
-


Bubaak-SpLit
-
-
+
-
-
-


CBMC
-
+
+
-
-
-


CPA-BAM-BnB
+
-
+
+
+
+


CPA-BAM-SMG
+
-
+
+
+
+


CPALockator
+
+
+
+
+
+


CPAchecker
+
+
+
+
+
+


CPV
-
-
+
-
-
-


Crux
-
-
+
-
-
-


CSeq
+
+
+
-
-
-


Dartagnan
-
+
-
-
-
-


Deagle
-
+
+
-
-
-


DIVINE
empty


EBF
empty


EmergenTheta
-
-
+
+
-
-


ESBMC-incr
-
+
+
-
-
-


ESBMC-kind
-
+
+
-
-
-


Frama-C-SV
empty


Gazer-Theta
+
-
+
-
-
-


Gdart-LLVM
-
-
+
-
-
-


Goblint
empty


Graves-CPA
+
+
+
+
+
-


Hornix
empty


Infer
empty


Korn
-
-
+
-
-
-


Lazy-CSeq
+
+
+
+
-
-


LF-checker
-
+
+
-
-
-


Locksmith
empty


Mopsa
empty


Nacpa
+
-
+
+
+
-


PeSCo-CPA
+
+
+
+
+
-


PIChecker
+
-
+
+
+
-


Pinaka
-
-
+
-
-
-


PredatorHP
-
-
-
-
-
-


PROTON
-
-
-
+
+
-


RacerF
empty


SV-sanitizers
empty


SVF-SVC
empty


Symbiotic
-
+
+
-
+
-


Theta
-
-
+
+
-
-


Thorn
empty


UAutomizer
+
+
+
+
+
-


UGemCutter
+
+
+
+
-
-


UKojak
+
-
+
+
-
-


UTaipan
+
+
+
+
-
-


VeriAbs
-
-
+
-
-
-


VeriAbsL
-
-
+
-
-
-


VeriOover
-
-
+
-
-
-




5. Correctness Proof Visualizations for SV-COMP Tools

This dataset provides a single representative none-empty correctness proof for each SV-COMP’2025 C verification tool, accompanied by the respective visualization. The focus is placed on elements that carry practical semantic value for developers -- conditions and invariants. A summary of supported proof elements across tools is presented in the corresponding evaluation table.

Table. 2. Evaluation of correctness proofs for all SV-COMP’2025 tools.




SV-COMP Tool
Invariants
Conditions


2LS
-
-


AISE
empty


AProVE
empty


BRICK
empty


Bubaak
empty


Bubaak-SpLit
empty


CBMC
+
-


CPA-BAM-BnB
+
+


CPA-BAM-SMG
+
+


CPALockator
empty


CPAchecker
+
+


CPV
empty


Crux
empty


CSeq
empty


Dartagnan
empty


Deagle
empty


DIVINE
empty


EBF
empty


EmergenTheta
empty


ESBMC-incr
empty


ESBMC-kind
empty


Frama-C-SV
empty


Gazer-Theta
empty


Gdart-LLVM
empty


Goblint
+
+


Graves-CPA
+
+


Hornix
empty


Infer
empty


Korn
empty


Lazy-CSeq
empty


LF-checker
empty


Locksmith
empty


Mopsa
empty


Nacpa
+
+


PeSCo-CPA
+
+


PIChecker
+
+


Pinaka
empty


PredatorHP
empty


PROTON
+
+


RacerF
empty


SV-sanitizers
empty


SVF-SVC
empty


Symbiotic
empty


Theta
empty


Thorn
empty


UAutomizer
+
-


UGemCutter
-
-


UKojak
+
-


UTaipan
+
-


VeriAbs
empty


VeriAbsL
empty


VeriOover
empty