Witness Inspection

A description of this web service can be found in the CAV paper "Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses" (more material).

View and Validate the Witness

View Witness
Click on the button to verify this program using this witness, and inpect the validation results, e.g., explore the ARG or error path.

Input Given to this Service about the Witness (URL Query)

Key	Value
programName	sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
programSHA	ff55f9adf7612eb7761a222adf76d027352321d4db65b966bdb67ac5d5c497bd
witnessName	results-verified/uautomizer.2017-12-02_0106.logfiles/sv-comp18.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.files/witness.graphml
witnessSHA	a1b24a9ffeb0043671537c9346f2531695f849a542c88e79447902df8f766792

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/a1b24a9ffeb0043671537c9346f2531695f849a542c88e79447902df8f766792.json

Key	Value
architecture	64bit
creationtime	2017-12-02T00:26Z
producer	Automizer
program-sha256	ff55f9adf7612eb7761a222adf76d027352321d4db65b966bdb67ac5d5c497bd
programfile	/tmp/vcloud-vcloud-master/worker/working_dir_d6a4ae8d-cfe8-497d-96f5-18b63e9a4ed1/sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
programhash	f8ffbb8f3d03c8e31202656b63b73873cd29533c
sourcecodelang	C
specification	CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file	witnessFileByHash/a1b24a9ffeb0043671537c9346f2531695f849a542c88e79447902df8f766792.graphml
witness-sha256	a1b24a9ffeb0043671537c9346f2531695f849a542c88e79447902df8f766792
witness-size	82693
witness-type	correctness_witness

Available Results for the Program from Witness Store SV-COMP '24

Trying to find witnesses for program (ff55f9adf7612eb7761a222adf76d027352321d4db65b966bdb67ac5d5c497bd, sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, ff55f9adf7612eb7761a222adf76d027352321d4db65b966bdb67ac5d5c497bd
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ff55f9adf7612eb7761a222adf76d027352321d4db65b966bdb67ac5d5c497bd.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness

Available Results for the Program from Witness Store SV-COMP '23

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, ff55f9adf7612eb7761a222adf76d027352321d4db65b966bdb67ac5d5c497bd
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ff55f9adf7612eb7761a222adf76d027352321d4db65b966bdb67ac5d5c497bd.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness

Available Results for the Program from Witness Store SV-COMP '22

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, ff55f9adf7612eb7761a222adf76d027352321d4db65b966bdb67ac5d5c497bd
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ff55f9adf7612eb7761a222adf76d027352321d4db65b966bdb67ac5d5c497bd.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness

Available Results for the Program from Witness Store SV-COMP '21

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, ff55f9adf7612eb7761a222adf76d027352321d4db65b966bdb67ac5d5c497bd
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ff55f9adf7612eb7761a222adf76d027352321d4db65b966bdb67ac5d5c497bd.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness

Available Results for the Program from Witness Store SV-COMP '20

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, ff55f9adf7612eb7761a222adf76d027352321d4db65b966bdb67ac5d5c497bd
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ff55f9adf7612eb7761a222adf76d027352321d4db65b966bdb67ac5d5c497bd.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness

Available Results for the Program from Witness Store SV-COMP '19

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, ff55f9adf7612eb7761a222adf76d027352321d4db65b966bdb67ac5d5c497bd
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ff55f9adf7612eb7761a222adf76d027352321d4db65b966bdb67ac5d5c497bd.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness

Available Results for the Program from Witness Store SV-COMP '18

Found 16 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, ff55f9adf7612eb7761a222adf76d027352321d4db65b966bdb67ac5d5c497bd
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ff55f9adf7612eb7761a222adf76d027352321d4db65b966bdb67ac5d5c497bd.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
0dcaa23	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Taipan	83	2017-12-02T16:42Z
daa2af0	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Kojak	83	2017-12-02T17:45Z
a0dcf9f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0 kind	4	2017-12-02T03:30:43.585931
c31e70d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn	4	2017-11-30T23:24:10+01:00
1b91d0a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	31	2017-12-03T07:12:21+01:00	0c918e0
e14df0e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	31	2017-12-03T03:10:16+01:00	7538c48
04fa9af	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	31	2017-12-03T00:56:51+01:00	581d9e9
ceb61ec	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	31	2017-12-02T09:12:07+01:00	e131cad
5e99b1f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	31	2017-12-01T06:58:43+01:00	fa56144
737cac9	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	31	2017-12-01T06:37:39+01:00	4448008
da950f2	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	31	2017-12-01T05:35:53+01:00	54053da
c39da9b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	31	2017-11-30T23:49:20+01:00
e5b1575	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26758M	14	2017-11-30T16:45:07+01:00
40104f4	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26725	31	2017-11-30T16:42:56+01:00
0398155	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker (unknown version)	21	2017-12-02T04:20:40+01:00
a1b24a9	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Automizer	83	2017-12-02T00:26Z

Available Results for the Program from Witness Store SV-COMP '17

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, ff55f9adf7612eb7761a222adf76d027352321d4db65b966bdb67ac5d5c497bd
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ff55f9adf7612eb7761a222adf76d027352321d4db65b966bdb67ac5d5c497bd.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness