Demonstrating Witness Visualization with the Witness Visualizer Tool

We have three datasets that display visualized SV-COMP witnesses generated with the help of the Witness Visualizer tool. Each dataset comprises two directories: witnesses, which contains the original witnesses provided by SVCOMP tools, and visualization, which contains our visual representations of the respective witnesses in HTML format. The visualization file name contains the prefix error_trace-, for example, error_trace-witness.2ls.html corresponds to a witness named witness.2ls.graphml.

1. Expert Evaluation of Relevant Elements for SV-COMP Properties (dataset_1.zip)

This dataset comprises a selected witness for each SV-COMP property (ReachSafety, MemSafety, Termination, NoOverflow, ConcurrencySafety). The witnesses are presented in the following table:

Witness
SV-COMP Tool
Property
Mandatory elements
Description

witness.memory.graphml
CPA-BAM-SMG
MemSafety
Assumptions, conditions, function calls
There is an invalid pointer being freed in this line. Using function calls to append helps clarify the structure of the list, while assumptions indicate which branch was chosen

witness.overflow.graphml
Graves-CPA
NoOverflow
Assumptions
The witness showcases an explicit (-2147483648, which represents the minimal value for the int type), which has the potential to cause overflow in specific program.

witness.termination.graphml
CPAChecker
NoTermination
Assumptions, conditions
There is a condition leading to an infinite loop.

witness.unreach.graphml
CPAChecker
ReachSafety
Function calls
The error trace suggests that the same mutex was locked twice, which could result in a potential deadlock.

witness.concurrency.graphml
CPAChecker
ConcurrencySafety
Function calls, thread operations
The error trace illustrates the creation of threads and highlights the assignments made within each thread that ultimately resulted in the violation of the property.

2. Overall thoroughness for all SV-COMP tools (dataset_2.zip)

This dataset includes a single random witness for each SV-COMP tool, accompanied by its corresponding visualization. The visualizations showcase the various witness elements such as function calls, conditions, assumptions, thread specifics, and other operations. Cells marked with +/- indicate that some elements were present in the error trace, but not all of them. All witnesses are presented in the table below:

Witness
SV-COMP Tool
Function calls
Threads
Assumptions
Conditions
Link to sources

witness.2ls.graphml
2LS
-
-
+
-
+

witness.aprove.graphml
AProVE (2022)
-
-
-
+
+

witness.brick.graphml
BRICK
-
-
+
-
+

witness.bubaak.graphml
Bubaak
-
-
+
-
+

witness.cbmc.graphml
CBMC
-
+
+
-
+

witness.cpa-bam-bnb.graphml
CPA-BAM-BnB
+
-
+
+
+

witness.cpa-bam-smg.graphml
CPA-BAM-SMG
+
-
+
+
+

witness.cpalockator.graphml
CPALockator
+
+
+
+
+

witness.cpachecker.graphml
CPAChecker
+
+
+
+
+

witness.crux.graphml
Crux
-
-
+
-
+

witness.cseq.graphml
Cseq
+
+
+
-
+

witness.dartagnan.graphml
Dartagnan
-
+
-
-
+

witness.deagle.graphml
Deagle
-
+
+
-
+

-
DIVINE
empty

-
EBF
empty

witness.esbmc-incr.graphml
ESBMC-incr
-
+
+
-
+

witness.esbmc-kind.graphml
ESBMC-kind
-
+
+
-
+

-
Frama-C-SV
empty

witness.gazer-theta.graphml
Gazer-Theta
+
-
+
-
wrong path

witness.gdart.graphml
Gdart-LLVM
-
-
+
-
+

-
Goblint
empty

witness.graves_cpa.graphml
Graves-CPA
+
+
+
+
+

witness.graves_par.graphml
Graves-Par
+
+
+
+
+

-
Infer
empty

witness.korn.graphml
Korn
-
-
+
-
+

witness.lart.graphml
LART (2022)
-
-
+
-
+

witness.lazy-cseq.graphml
Lazy-CSeq
+
+
+
+
+

witness.lfchecker.graphml
LF-checker
-
+
+
-
+

-
Locksmith
empty

-
Mopsa
empty

witness.pesco_cpa.graphml
PeSCo-CPA
+
+
+
+
+

witness.pichecker.graphml
PIChecker
+
-
+
+
+

witness.pinaka.graphml
Pinaka
-
-
+
-
+

witness.predator.graphml
PredatorHP
-
-
-
-
+

-
SESL (2022)
empty

witness.smack.graphml
SMACK (until 2022)
-
-
+
-
+

witness.symbiotic.graphml
Symbiotic
-
+
+
-
+

witness.theta.graphml
Theta
different format

witness.uatomozer.graphml
UAutomizer
+/-
+
+
+
+

witness.ucutter.graphml
UgemCutter
+/-
+
+
+
+

witness.ukojak.graphml
UKojak
+/-
-
+
+
+

witness.utaipan.graphml
UTaipan
+/-
+
+
+
+

witness.veriabs.graphml
VeriAbs
-
-
+
-
wrong path

witness.veriabsl.graphml
VeriAbsL
+
-
+
+
wrong path

witness.verifuzz.graphml
VeriFuzz
-
-
+
-
+

witness.verioover.graphml
VeriOover
-
-
+
-
+

3. A known bug (dataset_3.zip)

This dataset contains witnesses for a known bug from SVCOMP (linux-3.14--drivers--usb--misc--adutux.ko.cil.i) involving a data race on dev->udev, where concurrent writes occur without corresponding locks. Only two tools were able to solve the corresponding verification task: ESBMC-kind and CPALockator. The ESBMC error trace (witness.esbmc_2020.graphml) includes only thread specifics and assumptions, while the CPALockator witness (witness.lockator.graphml) comprises all witness elements and is presented in a human-readable format.