Demonstrations of witness visualization using the Witness Visualizer Tool

We have three datasets that display visualized SVCOMP 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. Overall thoroughness for all SVCOMP tools (dataset_1.zip) This dataset includes a single random witness for each SVCOMP 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 Control 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 (until 2022) 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 - - + - + 2. Thoroughness by property (dataset_2.zip) This dataset comprises a selected witness for each SVCOMP property (ReachSafety, MemSafety, Termination, NoOverflow, ConcurrencySafety). The witnesses are presented in the following table: Witness SV-COMP Tool Property Mandatory elements Description witness.smg_memory.graphml CPA-BAM-SMG MemSafety Assumptions / conditions, function calls There is a double free operation. Employing function calls append aids in comprehending the structure of the list, while assumptions reveal which branch was chosen. witness.graves_overflow.graphml Graves-CPA NoOverflow Assumptions / conditions 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.cpachecker_termination.graphml CPAChecker NoTermination Assumptions / conditions There is a condition leading to an infinite loop. witness.cpachecker_unreach.graphml CPAChecker ReachSafety Function calls The error trace indicates a potential scenario where a mutex was unlocked without the corresponding mutex_unlock operation. witness.cpachecker_conc.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. 3. 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.