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

The following keys are missing in the witness XML file: witness-type, sourcecodelang, producer, specification, programfile, programhash, architecture.

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

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

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

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

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

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

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

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

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

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

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

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

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
4500b2f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Symbiotic	1	2018-12-08T08:58 CET (sv-comp)
2096cef	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	SMACK 1.9.3	3	2018-12-08T19:13:06
794e4e2	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Pinaka	3	2018-12-07T06:32 CET (sv-comp)
845b1ad	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	6	2018-12-10T19:55:18+01:00	fa06907
a477e3f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	6	2018-12-09T21:20:59+01:00	50a2342
076ace2	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	6	2018-12-08T23:28:55+01:00	4500b2f
78f3d3b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	6	2018-12-08T22:01:33+01:00	2096cef
4ae4d08	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	6	2018-12-07T16:52:55+01:00	794e4e2

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

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

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
6f5b481	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Symbiotic	1	2017-12-02T12:20 CET (sv-comp)
df1d55f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Map2Check	4	2017-12-01T21:44 CET (sv-comp)
9ed32c5	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.12-svcomp17	4	2017-11-02T13:16:17+05:30
3e6b185	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	6	2017-12-03T04:44:05+01:00	65a8335
3f2d4a8	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	6	2017-12-02T20:18:48+01:00	a18bc2a
3e6f87e	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	6	2017-12-01T22:19:44+01:00	72c2275

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

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