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/f399afb514d44d5f759feca5f8497f21c5b3ac1f44f6665b4a01b84d9851475c.json

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

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--block--paride--bpck.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, a4360de354e9ea6a9cbf993dd92d0e2603e18aa3d8e033f7acb71c7db2c97019
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/a4360de354e9ea6a9cbf993dd92d0e2603e18aa3d8e033f7acb71c7db2c97019.json

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--block--paride--bpck.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, a4360de354e9ea6a9cbf993dd92d0e2603e18aa3d8e033f7acb71c7db2c97019
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/a4360de354e9ea6a9cbf993dd92d0e2603e18aa3d8e033f7acb71c7db2c97019.json

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--block--paride--bpck.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, a4360de354e9ea6a9cbf993dd92d0e2603e18aa3d8e033f7acb71c7db2c97019
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/a4360de354e9ea6a9cbf993dd92d0e2603e18aa3d8e033f7acb71c7db2c97019.json

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--block--paride--bpck.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, a4360de354e9ea6a9cbf993dd92d0e2603e18aa3d8e033f7acb71c7db2c97019
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/a4360de354e9ea6a9cbf993dd92d0e2603e18aa3d8e033f7acb71c7db2c97019.json

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--block--paride--bpck.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, a4360de354e9ea6a9cbf993dd92d0e2603e18aa3d8e033f7acb71c7db2c97019
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/a4360de354e9ea6a9cbf993dd92d0e2603e18aa3d8e033f7acb71c7db2c97019.json

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--block--paride--bpck.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, a4360de354e9ea6a9cbf993dd92d0e2603e18aa3d8e033f7acb71c7db2c97019
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/a4360de354e9ea6a9cbf993dd92d0e2603e18aa3d8e033f7acb71c7db2c97019.json

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

Found 8 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--block--paride--bpck.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, a4360de354e9ea6a9cbf993dd92d0e2603e18aa3d8e033f7acb71c7db2c97019
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/a4360de354e9ea6a9cbf993dd92d0e2603e18aa3d8e033f7acb71c7db2c97019.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
f399afb	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Taipan	1917	2017-12-03T04:56Z
5892ac9	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Kojak	1957	2017-12-02T20:01Z
b1ae02f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0 kind	4	2017-12-01T19:05:27.252622
ef58588	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	304	2017-11-30T12:12:08+01:00
ecd6a01	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26758M	21	2017-12-01T03:53:04+01:00
4c554d2	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26725	304	2017-11-30T12:48:19+01:00
fb48cff	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker (unknown version)	267	2017-12-01T23:44:19+01:00
1620b84	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Automizer	1917	2017-12-02T13:04Z

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--block--paride--bpck.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, a4360de354e9ea6a9cbf993dd92d0e2603e18aa3d8e033f7acb71c7db2c97019
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/a4360de354e9ea6a9cbf993dd92d0e2603e18aa3d8e033f7acb71c7db2c97019.json