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)

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/fd9ab0e871d8919f8c68ec16159de3ba72f8d5327234246417a24b0691be160e.json

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

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i, b69fcbb389a564a80fd5bec3fc42b329081e46d2335e4c5413cd6cbc636d6517
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/b69fcbb389a564a80fd5bec3fc42b329081e46d2335e4c5413cd6cbc636d6517.json

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

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i, b69fcbb389a564a80fd5bec3fc42b329081e46d2335e4c5413cd6cbc636d6517
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/b69fcbb389a564a80fd5bec3fc42b329081e46d2335e4c5413cd6cbc636d6517.json

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

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i, b69fcbb389a564a80fd5bec3fc42b329081e46d2335e4c5413cd6cbc636d6517
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/b69fcbb389a564a80fd5bec3fc42b329081e46d2335e4c5413cd6cbc636d6517.json

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

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i, b69fcbb389a564a80fd5bec3fc42b329081e46d2335e4c5413cd6cbc636d6517
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/b69fcbb389a564a80fd5bec3fc42b329081e46d2335e4c5413cd6cbc636d6517.json

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

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i, b69fcbb389a564a80fd5bec3fc42b329081e46d2335e4c5413cd6cbc636d6517
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/b69fcbb389a564a80fd5bec3fc42b329081e46d2335e4c5413cd6cbc636d6517.json

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

Found 10 witnesses for program sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i, b69fcbb389a564a80fd5bec3fc42b329081e46d2335e4c5413cd6cbc636d6517
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/b69fcbb389a564a80fd5bec3fc42b329081e46d2335e4c5413cd6cbc636d6517.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
3bd0278	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Symbiotic	1	2018-12-08T08:34 CET (sv-comp)
2f4b5f7	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	SMACK 1.9.3	3	2018-12-08T00:04:17
08e4661	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn b8d6131600+	208	2018-12-07T04:02:17+01:00
b9aa6be	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	208	2018-12-08T23:27:52+01:00	3bd0278
b5696ca	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	208	2018-12-08T21:42:42+01:00	2f4b5f7
1c8ba77	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	208	2018-12-08T05:51:42+01:00	08e4661
2c14e4e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	208	2018-12-06T09:05:36+01:00	89131b2
89131b2	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	208	2018-12-05T17:45:35+01:00
420e65e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	208	2018-12-05T15:10:40+01:00	70cda40
70cda40	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29794	318	2018-12-05T08:28:39+01:00

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

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i, b69fcbb389a564a80fd5bec3fc42b329081e46d2335e4c5413cd6cbc636d6517
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/b69fcbb389a564a80fd5bec3fc42b329081e46d2335e4c5413cd6cbc636d6517.json

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

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i, b69fcbb389a564a80fd5bec3fc42b329081e46d2335e4c5413cd6cbc636d6517
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/b69fcbb389a564a80fd5bec3fc42b329081e46d2335e4c5413cd6cbc636d6517.json