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_compare_true-unreach-call_ground.i, 7ec38ef9746a64eb3611c75b9e9a23cafa6320f1c08e7b81aaa2e061ca12ed2c
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/7ec38ef9746a64eb3611c75b9e9a23cafa6320f1c08e7b81aaa2e061ca12ed2c.json

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

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

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

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

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

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

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

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

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

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

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
6fae7c7	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Symbiotic	1	2018-12-08T00:36 CET (sv-comp)
d5a1fa4	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	SMACK 1.9.3	3	2018-12-08T08:12:30
5078588	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn b8d6131600+	7	2018-12-07T05:58:25+01:00
97993fc	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	7	2018-12-10T20:31:22+01:00	345188b
dd0bec6	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	7	2018-12-09T21:20:54+01:00	1f3e9a1
91504ab	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	7	2018-12-08T23:38:43+01:00	6fae7c7
d4e9bec	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	7	2018-12-08T21:55:48+01:00	d5a1fa4
1df73a1	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	7	2018-12-08T05:32:14+01:00	5078588

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

Found 4 witnesses for program sv-benchmarks/c/array-examples/standard_compare_true-unreach-call_ground.i, 7ec38ef9746a64eb3611c75b9e9a23cafa6320f1c08e7b81aaa2e061ca12ed2c
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/7ec38ef9746a64eb3611c75b9e9a23cafa6320f1c08e7b81aaa2e061ca12ed2c.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
b849461	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	Map2Check	4	2017-12-01T20:27 CET (sv-comp)
db833b8	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.12-svcomp17	4	2017-11-02T13:16:17+05:30
11c604f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	7	2017-12-03T04:32:52+01:00	a7d5879
b8e338d	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.6.1-svn 26773	7	2017-12-01T22:28:35+01:00	f3dd564

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

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