Artifact: Visualization of Verification Results for Linux Kernel Benchmarks with CV

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/MvOt9xGJ1OI. 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