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/2018/results/witnessInfoByHash/84922c5565fe60dfaa5e29111ee88af3a1e5e6866d0495c5c8b2739ad1495326.json

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

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i, f891d160a7b04e861aeef4d35712aa701d63889019d2e4e2e8bd9f7b1cdec891
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f891d160a7b04e861aeef4d35712aa701d63889019d2e4e2e8bd9f7b1cdec891.json

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

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i, f891d160a7b04e861aeef4d35712aa701d63889019d2e4e2e8bd9f7b1cdec891
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f891d160a7b04e861aeef4d35712aa701d63889019d2e4e2e8bd9f7b1cdec891.json

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

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i, f891d160a7b04e861aeef4d35712aa701d63889019d2e4e2e8bd9f7b1cdec891
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f891d160a7b04e861aeef4d35712aa701d63889019d2e4e2e8bd9f7b1cdec891.json

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

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i, f891d160a7b04e861aeef4d35712aa701d63889019d2e4e2e8bd9f7b1cdec891
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f891d160a7b04e861aeef4d35712aa701d63889019d2e4e2e8bd9f7b1cdec891.json

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

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i, f891d160a7b04e861aeef4d35712aa701d63889019d2e4e2e8bd9f7b1cdec891
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f891d160a7b04e861aeef4d35712aa701d63889019d2e4e2e8bd9f7b1cdec891.json

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

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i, f891d160a7b04e861aeef4d35712aa701d63889019d2e4e2e8bd9f7b1cdec891
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f891d160a7b04e861aeef4d35712aa701d63889019d2e4e2e8bd9f7b1cdec891.json

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

Found 13 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i, f891d160a7b04e861aeef4d35712aa701d63889019d2e4e2e8bd9f7b1cdec891
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f891d160a7b04e861aeef4d35712aa701d63889019d2e4e2e8bd9f7b1cdec891.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
82131be	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Taipan	669	2017-12-03T04:49Z
836a779	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0 kind	3	2017-12-01T17:59:34.955684
a01ac33	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	3589	2017-12-03T07:02:23+01:00	2894e3e
6065b9a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	3589	2017-12-03T01:20:37+01:00	aa1f85d
a8f7b2f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	3589	2017-12-02T07:16:05+01:00	fdcb724
2de2f6e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	3589	2017-12-01T05:34:13+01:00	e71d004
328da2a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	3589	2017-12-01T05:14:52+01:00	9a780df
a67bf51	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	3589	2017-12-01T05:09:38+01:00	8ebb39f
ad46a7c	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	3589	2017-11-30T21:53:38+01:00
e8be784	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26758M	12	2017-11-30T17:01:46+01:00
c27680a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26725	3589	2017-11-30T23:16:05+01:00
5de02db	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker (unknown version)	208	2017-12-01T22:33:09+01:00
84922c5	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Automizer	10297	2017-12-02T11:22Z

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

Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i, f891d160a7b04e861aeef4d35712aa701d63889019d2e4e2e8bd9f7b1cdec891
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f891d160a7b04e861aeef4d35712aa701d63889019d2e4e2e8bd9f7b1cdec891.json