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

This witness was created for this program (cf. table above, 6740fe562124c4d4cd2cdeedf72ebc890c2f848e4bce7fcae3826fc132296893).

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

Found 0 witnesses for program sv-benchmarks/c/array-examples/standard_two_index_05_true-unreach-call.i, 6740fe562124c4d4cd2cdeedf72ebc890c2f848e4bce7fcae3826fc132296893
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/6740fe562124c4d4cd2cdeedf72ebc890c2f848e4bce7fcae3826fc132296893.json

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

Found 0 witnesses for program sv-benchmarks/c/array-examples/standard_two_index_05_true-unreach-call.i, 6740fe562124c4d4cd2cdeedf72ebc890c2f848e4bce7fcae3826fc132296893
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/6740fe562124c4d4cd2cdeedf72ebc890c2f848e4bce7fcae3826fc132296893.json

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

Found 0 witnesses for program sv-benchmarks/c/array-examples/standard_two_index_05_true-unreach-call.i, 6740fe562124c4d4cd2cdeedf72ebc890c2f848e4bce7fcae3826fc132296893
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/6740fe562124c4d4cd2cdeedf72ebc890c2f848e4bce7fcae3826fc132296893.json

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

Found 0 witnesses for program sv-benchmarks/c/array-examples/standard_two_index_05_true-unreach-call.i, 6740fe562124c4d4cd2cdeedf72ebc890c2f848e4bce7fcae3826fc132296893
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/6740fe562124c4d4cd2cdeedf72ebc890c2f848e4bce7fcae3826fc132296893.json

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

Found 3 witnesses for program sv-benchmarks/c/array-examples/standard_two_index_05_true-unreach-call.i, 6740fe562124c4d4cd2cdeedf72ebc890c2f848e4bce7fcae3826fc132296893
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/6740fe562124c4d4cd2cdeedf72ebc890c2f848e4bce7fcae3826fc132296893.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
60034bf	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Pinaka	3	2019-12-03T23:58 CET (comp)
9602bcb	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	7	2019-12-08T00:51:01+01:00	a0e9bbe
9502f0b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.9 / witnessValidation	7	2019-12-04T02:22:40+01:00	60034bf

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

Found 8 witnesses for program sv-benchmarks/c/array-examples/standard_two_index_05_true-unreach-call.i, 6740fe562124c4d4cd2cdeedf72ebc890c2f848e4bce7fcae3826fc132296893
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6740fe562124c4d4cd2cdeedf72ebc890c2f848e4bce7fcae3826fc132296893.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
28d8cdb	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Symbiotic	1	2018-12-08T09:27 CET (sv-comp)
4f2087c	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	SMACK 1.9.3	3	2018-12-08T03:12:49
3a0243a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Pinaka	3	2018-12-07T09:01 CET (sv-comp)
5a10584	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	7	2018-12-10T20:21:08+01:00	a27642d
81d0c4c	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	7	2018-12-09T21:21:16+01:00	17b8fcc
b6ae9ae	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	7	2018-12-08T23:27:44+01:00	28d8cdb
e5e7c9d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	7	2018-12-08T21:58:31+01:00	4f2087c
f92942f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	7	2018-12-07T16:53:13+01:00	3a0243a

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

Found 4 witnesses for program sv-benchmarks/c/array-examples/standard_two_index_05_true-unreach-call.i, 6740fe562124c4d4cd2cdeedf72ebc890c2f848e4bce7fcae3826fc132296893
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/6740fe562124c4d4cd2cdeedf72ebc890c2f848e4bce7fcae3826fc132296893.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
6c5ca61	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Symbiotic	1	2017-12-02T17:05 CET (sv-comp)
155aa9d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.12-svcomp17	4	2017-11-02T13:16:17+05:30
3bb73b0	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	7	2017-12-03T04:34:38+01:00	0b0c220
49c053a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	7	2017-12-02T20:06:37+01:00	34e3bf1

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

Found 0 witnesses for program sv-benchmarks/c/array-examples/standard_two_index_05_true-unreach-call.i, 6740fe562124c4d4cd2cdeedf72ebc890c2f848e4bce7fcae3826fc132296893
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/6740fe562124c4d4cd2cdeedf72ebc890c2f848e4bce7fcae3826fc132296893.json