Witness Visualizer – A Tool for Manual Inspection of Software Verification Results

Witness Visualizer is designed to provide an interactive, human-readable visualization of software verification witnesses, conforming to the SV-COMP format. It enables manual inspection and interpretation of verification results, assisting both tool developers and end users in understanding error traces, identifying real bugs, and improving witness quality. This artifact includes the following components: Dataset 1:A collection of non-empty witnesses generated by SV-COMP tools along with their corresponding visualizations created by Witness Visualizer.The dataset is organized into two directories: witnesses/: contains the original witness files in GraphML format. visualization/: contains the HTML visualizations produced from these witnesses.Each visualization is named using the prefix error_trace-. For example, error_trace-witness.2ls.html corresponds to the input witness witness.2ls.graphml, generated by the 2LS verifier. Dataset 2:Witnesses for a known concurrency bug in the SV-COMP task linux-3.14--drivers--usb--misc--adutux.ko.cil.i, which involves a data race on the dev->udev field (two concurrent write accesses without proper locking).Only two verifiers successfully solved this task, and the artifact includes the corresponding witnesses: witness.esbmc_2020.graphml (from ESBMC-kind) includes thread context and assumptions. witness.lockator.graphml (from CPALockator) provides a complete witness including violation hints, enabling a more human-readable visualization. Dataset 3:Visualizations for witnesses generated during the verification of Linux kernel modules against various properties, such as: Memory safety Concurrency safety Unreachability of error functions (for example, checking that a call to disable() is preceded by a corresponding call to enable()). Dockerfile:A standalone setup of Witness Visualizer is provided via a Dockerfile. It enables local generation of witness visualizations without needing to deploy the web interface.To run the visualizer: scripts/visualize_witnesses.py --witness witness.graphml --result-dir results/ --source-dir sv-benchmarks The visualization output will be saved in the results/ directory.For detailed usage instructions in standalone mode, refer to: https://github.com/ispras/cv/blob/master/docs/witness_visualizer.md If you want to explore the visualization of an entire benchmark run - including error traces, proofs, verifier logs, coverage information, and overall statistics - you need to set up the CVV web interface according to its instructions.