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

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

Found 0 witnesses for program sv-benchmarks/c/array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i, 7befc44f16850f1dc3ed6daeae6724dec23004ceebef936011646f584a3d7bad
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/7befc44f16850f1dc3ed6daeae6724dec23004ceebef936011646f584a3d7bad.json

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

Found 0 witnesses for program sv-benchmarks/c/array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i, 7befc44f16850f1dc3ed6daeae6724dec23004ceebef936011646f584a3d7bad
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/7befc44f16850f1dc3ed6daeae6724dec23004ceebef936011646f584a3d7bad.json

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

Found 0 witnesses for program sv-benchmarks/c/array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i, 7befc44f16850f1dc3ed6daeae6724dec23004ceebef936011646f584a3d7bad
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/7befc44f16850f1dc3ed6daeae6724dec23004ceebef936011646f584a3d7bad.json

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

Found 0 witnesses for program sv-benchmarks/c/array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i, 7befc44f16850f1dc3ed6daeae6724dec23004ceebef936011646f584a3d7bad
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/7befc44f16850f1dc3ed6daeae6724dec23004ceebef936011646f584a3d7bad.json

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

Found 3 witnesses for program sv-benchmarks/c/array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i, 7befc44f16850f1dc3ed6daeae6724dec23004ceebef936011646f584a3d7bad
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/7befc44f16850f1dc3ed6daeae6724dec23004ceebef936011646f584a3d7bad.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
5961cda	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Symbiotic	1	2019-12-01 03:51:21
f0a5159	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Pinaka	65383	2019-12-04T00:49 CET (comp)
7f2a499	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	Pinaka	3	2019-12-03T22:51 CET (comp)

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

Found 6 witnesses for program sv-benchmarks/c/array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i, 7befc44f16850f1dc3ed6daeae6724dec23004ceebef936011646f584a3d7bad
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/7befc44f16850f1dc3ed6daeae6724dec23004ceebef936011646f584a3d7bad.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
09fc6c3	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Symbiotic	1	2018-12-08T11:28 CET (sv-comp)
0dd960a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	SMACK 1.9.3	4	2018-12-08T07:59:18
c7819d5	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Pinaka	72584	2018-12-06T23:46 CET (sv-comp)
b1fdac4	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	7	2018-12-06T10:11:04+01:00	11b9137
d914ccd	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	Symbiotic	1	2018-12-08T04:00 CET (sv-comp)
ccd5bd7	Inspect		CHECK( init(main()), LTL(F end) )	correctness_witness	Pinaka	3	2018-12-07T05:31 CET (sv-comp)

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

Found 3 witnesses for program sv-benchmarks/c/array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i, 7befc44f16850f1dc3ed6daeae6724dec23004ceebef936011646f584a3d7bad
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/7befc44f16850f1dc3ed6daeae6724dec23004ceebef936011646f584a3d7bad.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
194e852	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	VIAP	79037	2017-12-03T03:48 CET (sv-comp)
a57dab1	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Symbiotic	1	2017-12-02T12:30 CET (sv-comp)
20fd61f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Map2Check	4	2017-12-01T20:08 CET (sv-comp)

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

Found 0 witnesses for program sv-benchmarks/c/array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i, 7befc44f16850f1dc3ed6daeae6724dec23004ceebef936011646f584a3d7bad
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/7befc44f16850f1dc3ed6daeae6724dec23004ceebef936011646f584a3d7bad.json