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

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

Found 0 witnesses for program sv-benchmarks/c/array-examples/standard_copy5_true-unreach-call_ground.i, 45e3deddc87556836cbc96733ed004ee97a4800e87e6f78f399e0e571b55a25c
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/45e3deddc87556836cbc96733ed004ee97a4800e87e6f78f399e0e571b55a25c.json

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

Found 0 witnesses for program sv-benchmarks/c/array-examples/standard_copy5_true-unreach-call_ground.i, 45e3deddc87556836cbc96733ed004ee97a4800e87e6f78f399e0e571b55a25c
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/45e3deddc87556836cbc96733ed004ee97a4800e87e6f78f399e0e571b55a25c.json

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

Found 0 witnesses for program sv-benchmarks/c/array-examples/standard_copy5_true-unreach-call_ground.i, 45e3deddc87556836cbc96733ed004ee97a4800e87e6f78f399e0e571b55a25c
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/45e3deddc87556836cbc96733ed004ee97a4800e87e6f78f399e0e571b55a25c.json

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

Found 0 witnesses for program sv-benchmarks/c/array-examples/standard_copy5_true-unreach-call_ground.i, 45e3deddc87556836cbc96733ed004ee97a4800e87e6f78f399e0e571b55a25c
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/45e3deddc87556836cbc96733ed004ee97a4800e87e6f78f399e0e571b55a25c.json

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

Found 3 witnesses for program sv-benchmarks/c/array-examples/standard_copy5_true-unreach-call_ground.i, 45e3deddc87556836cbc96733ed004ee97a4800e87e6f78f399e0e571b55a25c
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/45e3deddc87556836cbc96733ed004ee97a4800e87e6f78f399e0e571b55a25c.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
e8e4ce4	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Pinaka	3	2019-12-03T23:28 CET (comp)
69a8e43	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	11	2019-12-08T01:08:14+01:00	a4366f6
921011c	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	11	2019-12-04T02:22:36+01:00	e8e4ce4

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

Found 8 witnesses for program sv-benchmarks/c/array-examples/standard_copy5_true-unreach-call_ground.i, 45e3deddc87556836cbc96733ed004ee97a4800e87e6f78f399e0e571b55a25c
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/45e3deddc87556836cbc96733ed004ee97a4800e87e6f78f399e0e571b55a25c.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
38a35fe	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Symbiotic	1	2018-12-08T08:09 CET (sv-comp)
f05f88a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	SMACK 1.9.3	3	2018-12-07T21:34:05
716a9cb	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Pinaka	3	2018-12-07T08:38 CET (sv-comp)
289473f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	11	2018-12-10T20:18:02+01:00	2833657
a2e06f6	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	11	2018-12-09T21:21:32+01:00	cbaf611
5d47d4b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	11	2018-12-08T23:29:21+01:00	38a35fe
0488dad	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	11	2018-12-08T21:51:34+01:00	f05f88a
842a343	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	11	2018-12-07T16:53:55+01:00	716a9cb

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

Found 6 witnesses for program sv-benchmarks/c/array-examples/standard_copy5_true-unreach-call_ground.i, 45e3deddc87556836cbc96733ed004ee97a4800e87e6f78f399e0e571b55a25c
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/45e3deddc87556836cbc96733ed004ee97a4800e87e6f78f399e0e571b55a25c.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
022416d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Symbiotic	1	2017-12-02T02:13 CET (sv-comp)
ed6b30b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 3.1	13	2017-11-30T19:06 CET (sv-comp)
eba2e6d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.12-svcomp17	4	2017-11-02T13:16:17+05:30
c8dc3e6	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	11	2017-12-03T04:36:53+01:00	c157255
4f15578	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	11	2017-12-02T20:44:19+01:00	7b74e5a
b239272	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	11	2017-12-01T08:28:49+01:00	617e707

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

Found 0 witnesses for program sv-benchmarks/c/array-examples/standard_copy5_true-unreach-call_ground.i, 45e3deddc87556836cbc96733ed004ee97a4800e87e6f78f399e0e571b55a25c
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/45e3deddc87556836cbc96733ed004ee97a4800e87e6f78f399e0e571b55a25c.json