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
Input Given to this Service about the Witness (URL Query)
Key |
Value |
programName |
sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i |
programSHA |
5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142 |
witnessName |
results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-reachsafety.avg40_true-unreach-call.i.files/witness.graphml |
witnessSHA |
0a2956fed0b12ff9da9e281fb4db4d6b814dfceb06855499a4a74c430800c94d |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/0a2956fed0b12ff9da9e281fb4db4d6b814dfceb06855499a4a74c430800c94d.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-05T12:45:15.956219 |
producer |
DepthK v3.0 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_aac172ce-b21a-4c54-97e5-86d760dc5e3a/sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i |
programhash |
236dcd0ec5dd9ced1e4699159168b0146d1f3114 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/0a2956fed0b12ff9da9e281fb4db4d6b814dfceb06855499a4a74c430800c94d.graphml |
witness-sha256 |
0a2956fed0b12ff9da9e281fb4db4d6b814dfceb06855499a4a74c430800c94d |
witness-size |
3471 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142, sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i, 5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142, sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i, 5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142, sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i, 5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '21
Trying to find witnesses for program (5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142, sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i, 5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '20
Trying to find witnesses for program (5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142, sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i).
Found 8 witnesses for program sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i, 5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
e5f7ced |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
Pinaka |
3 |
2019-12-04T00:43 CET (comp) |
|
21358de |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
8 |
2019-12-11T20:17:15+01:00 |
22b3897 |
056e1e6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
8 |
2019-12-08T00:52:38+01:00 |
4a67e22 |
82cb0e8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
8 |
2019-12-06T01:44:03+01:00 |
7fc6752 |
c766465 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
8 |
2019-12-04T02:07:57+01:00 |
e5f7ced |
f09cec6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
8 |
2019-11-30T19:29:59+01:00 |
6145904 |
955cd3d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
8 |
2019-11-30T16:28:10+01:00 |
7d2e8b2 |
7d2e8b2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / svcomp20 |
22 |
2019-11-30T04:47:42+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142, sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i).
Found 14 witnesses for program sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i, 5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
acb5e8b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
Symbiotic |
1 |
2018-12-08T19:02 CET (sv-comp) |
|
037f4b1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
SMACK 1.9.3 |
3 |
2018-12-08T07:35:55 |
|
727be27 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
Pinaka |
3 |
2018-12-07T11:09 CET (sv-comp) |
|
bb35636 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
22 |
2018-12-07T21:53:03+01:00 |
|
f7498b6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-10T19:50:57+01:00 |
9e0b780 |
94c41c4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-09T21:21:15+01:00 |
d88cd27 |
cd45ea3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-08T23:24:50+01:00 |
acb5e8b |
ee530c4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-08T21:49:39+01:00 |
037f4b1 |
e4b5f16 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
10 |
2018-12-08T05:44:22+01:00 |
bb35636 |
b33061b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-08T02:36:06+01:00 |
73bf8f2 |
693f2e7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-07T16:53:47+01:00 |
727be27 |
e731d7e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-06T09:43:30+01:00 |
0a2956f |
f1d1d53 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
10 |
2018-12-06T09:27:50+01:00 |
d3cc162 |
d3cc162 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
22 |
2018-12-05T14:19:45+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142, sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i).
Found 9 witnesses for program sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i, 5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
e8a99a2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26758M |
311 |
2017-11-30T15:25:24+01:00 |
|
03ad2b3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26725 |
158 |
2017-11-30T12:38:26+01:00 |
|
6195c08 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker (unknown version) |
118 |
2017-12-01T22:40:36+01:00 |
|
adb29e5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
skink |
3 |
2017-12-01T23:26 CET (sv-comp) |
|
bb3f8bb |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
Symbiotic |
1 |
2017-12-01T23:03 CET (sv-comp) |
|
7d5393d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.12-svcomp17 |
4 |
2017-11-02T13:16:17+05:30 |
|
22fb72f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
8 |
2017-12-03T04:13:50+01:00 |
59399a3 |
b5eaee3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
8 |
2017-12-02T21:07:10+01:00 |
a7bc625 |
5d3d7af |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
8 |
2017-12-02T00:26:07+01:00 |
a1778ed |
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142, sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/avg40_true-unreach-call.i, 5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/5549adc9f67c1f549efc98acf62aebb513a405244ae86be397abac68fd272142.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |