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--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
programSHA	4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81
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--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.files/witness.graphml
witnessSHA	c7a65b0e508a8c5f75bbe16627ca5ab0af2641f00fa328d7659889daa7391bf4

Information about the Witness from Competition Database

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

Key	Value
architecture	64bit
creationtime	2017-12-02T07:13Z
producer	Automizer
program-sha256	4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81
programfile	/tmp/vcloud-vcloud-master/worker/working_dir_bd723ce2-670b-45db-9ccc-52bda5cae262/sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
programhash	7751ba17d43764b0c21a621e1cdadc91c0bab864
sourcecodelang	C
specification	CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file	witnessFileByHash/c7a65b0e508a8c5f75bbe16627ca5ab0af2641f00fa328d7659889daa7391bf4.graphml
witness-sha256	c7a65b0e508a8c5f75bbe16627ca5ab0af2641f00fa328d7659889daa7391bf4
witness-size	279504
witness-type	correctness_witness

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

Trying to find witnesses for program (4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81, sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpu--drm--i2c--sil164.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--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81.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--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81.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--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81.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--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81.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--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81.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--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81.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 15 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--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
5668064	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Taipan	280	2017-12-03T03:17Z
4c3171c	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Kojak	280	2017-12-02T21:07Z
f4a7a5c	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 4.6.0 kind	4	2017-12-01T15:16:06.437696
d710f47	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	76	2017-12-03T07:11:46+01:00	e15656a
dae275f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	76	2017-12-03T01:38:12+01:00	436ea99
5b6dc89	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	76	2017-12-02T23:36:28+01:00	997b97a
b4df138	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	76	2017-12-02T08:13:30+01:00	0d910f7
ad1a479	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	76	2017-12-01T06:41:18+01:00	98276c2
8c9a4c0	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	76	2017-12-01T06:05:57+01:00	0c31606
d3ff8f9	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	77	2017-12-01T05:48:06+01:00	e78b18b
a6913d7	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	77	2017-11-30T16:17:24+01:00
de737c7	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26758M	18	2017-11-30T18:45:56+01:00
f2fb4bf	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26725	76	2017-11-30T19:06:47+01:00
fdd4e98	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker (unknown version)	62	2017-12-02T11:36:03+01:00
c7a65b0	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Automizer	280	2017-12-02T07:13Z

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--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c, 4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/4534796805ca370b4ea1fd0c385e2122775dc6dea89c2293e6c87029b0229b81.json

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