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/34924f3340d91bc3a33ec2396ad47f16bdf114a15973972012867da37ea1b5b7.json

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

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

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

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

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

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

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

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

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

Found 0 witnesses for program sv-benchmarks/c/array-examples/standard_copy7_false-unreach-call_ground.i, 548034e8f8fd4ca610badc6ce79a94f65a5d1a355792158917e99dcda8b59fc0
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/548034e8f8fd4ca610badc6ce79a94f65a5d1a355792158917e99dcda8b59fc0.json

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

Found 2 witnesses for program sv-benchmarks/c/array-examples/standard_copy7_false-unreach-call_ground.i, 548034e8f8fd4ca610badc6ce79a94f65a5d1a355792158917e99dcda8b59fc0
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/548034e8f8fd4ca610badc6ce79a94f65a5d1a355792158917e99dcda8b59fc0.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
43a578a	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Symbiotic	1	2018-12-08T08:09 CET (sv-comp)
2e4a01b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	SMACK 1.9.3	3	2018-12-07T20:21:37

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

Found 5 witnesses for program sv-benchmarks/c/array-examples/standard_copy7_false-unreach-call_ground.i, 548034e8f8fd4ca610badc6ce79a94f65a5d1a355792158917e99dcda8b59fc0
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/548034e8f8fd4ca610badc6ce79a94f65a5d1a355792158917e99dcda8b59fc0.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
7f2681e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	VIAP	4	2017-12-03T04:02 CET (sv-comp)
e3afdfc	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	Symbiotic	1	2017-12-02T18:08 CET (sv-comp)
713d1a6	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	AFL	2	2017-12-02T18:28 CET (sv-comp)
35d0bc5	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	ESBMC 3.1	16	2017-12-01T01:17 CET (sv-comp)
4877f35	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	13	2017-12-01T08:37:18+01:00	7fba61d

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

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