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/9daa3566c96b86f3179462fd91e865d2808f4358b4aa56da7601f837ddf6933b.json

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

Found 0 witnesses for program sv-benchmarks/c/array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i, 5e2b9c7369816eca655fe8f1d7e5c9741f5aaaa5fcf7e33c2b90959c0c8142e0
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/5e2b9c7369816eca655fe8f1d7e5c9741f5aaaa5fcf7e33c2b90959c0c8142e0.json

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

Found 0 witnesses for program sv-benchmarks/c/array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i, 5e2b9c7369816eca655fe8f1d7e5c9741f5aaaa5fcf7e33c2b90959c0c8142e0
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/5e2b9c7369816eca655fe8f1d7e5c9741f5aaaa5fcf7e33c2b90959c0c8142e0.json

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

Found 0 witnesses for program sv-benchmarks/c/array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i, 5e2b9c7369816eca655fe8f1d7e5c9741f5aaaa5fcf7e33c2b90959c0c8142e0
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/5e2b9c7369816eca655fe8f1d7e5c9741f5aaaa5fcf7e33c2b90959c0c8142e0.json

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

Found 0 witnesses for program sv-benchmarks/c/array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i, 5e2b9c7369816eca655fe8f1d7e5c9741f5aaaa5fcf7e33c2b90959c0c8142e0
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/5e2b9c7369816eca655fe8f1d7e5c9741f5aaaa5fcf7e33c2b90959c0c8142e0.json

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

Found 0 witnesses for program sv-benchmarks/c/array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i, 5e2b9c7369816eca655fe8f1d7e5c9741f5aaaa5fcf7e33c2b90959c0c8142e0
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/5e2b9c7369816eca655fe8f1d7e5c9741f5aaaa5fcf7e33c2b90959c0c8142e0.json

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

Found 2 witnesses for program sv-benchmarks/c/array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i, 5e2b9c7369816eca655fe8f1d7e5c9741f5aaaa5fcf7e33c2b90959c0c8142e0
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/5e2b9c7369816eca655fe8f1d7e5c9741f5aaaa5fcf7e33c2b90959c0c8142e0.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
9fa5401	Inspect		CHECK( init(main()), LTL(G valid-memtrack) )	correctness_witness	CPAchecker 1.7-svn 29852	6	2018-12-06T06:30:00+01:00
5d07301	Inspect		CHECK( init(main()), LTL(G valid-free) )	correctness_witness	CPAchecker 1.7-svn b8d6131600+	6	2018-12-07T14:49:54+01:00

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

Found 4 witnesses for program sv-benchmarks/c/array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i, 5e2b9c7369816eca655fe8f1d7e5c9741f5aaaa5fcf7e33c2b90959c0c8142e0
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/5e2b9c7369816eca655fe8f1d7e5c9741f5aaaa5fcf7e33c2b90959c0c8142e0.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
9592d14	Inspect		CHECK( init(main()), LTL(G valid-memtrack) )	correctness_witness	Symbiotic	1	2017-12-02T23:57 CET (sv-comp)
e8829f4	Inspect		CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )	correctness_witness	Taipan	8	2017-12-03T06:53Z
d5fa4d6	Inspect		CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )	correctness_witness	Map2Check	4	2017-12-01T23:46 CET (sv-comp)
81e9e94	Inspect		CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )	correctness_witness	Kojak	8	2017-12-03T03:46Z

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

Found 0 witnesses for program sv-benchmarks/c/array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i, 5e2b9c7369816eca655fe8f1d7e5c9741f5aaaa5fcf7e33c2b90959c0c8142e0
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/5e2b9c7369816eca655fe8f1d7e5c9741f5aaaa5fcf7e33c2b90959c0c8142e0.json