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/max20_true-unreach-call.i |
| programSHA |
bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174 |
| witnessName |
results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-reachsafety.max20_true-unreach-call.i.files/witness.graphml |
| witnessSHA |
a092ffe0c93525a0fac6413fa0682abfc4018f20f096945ebd1cab1496ba712d |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/a092ffe0c93525a0fac6413fa0682abfc4018f20f096945ebd1cab1496ba712d.json
| Key |
Value |
| architecture |
32bit |
| creationtime |
2018-12-05T20:57:55.188918 |
| producer |
DepthK v3.0 |
| programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_6c75da0e-bd76-4c1d-ab2a-aee262ac7d79/sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i |
| programhash |
67d74bcd4ddf537770c7e039af1f9d86f962eaff |
| sourcecodelang |
C |
| specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
| witness-file |
witnessFileByHash/a092ffe0c93525a0fac6413fa0682abfc4018f20f096945ebd1cab1496ba712d.graphml |
| witness-sha256 |
a092ffe0c93525a0fac6413fa0682abfc4018f20f096945ebd1cab1496ba712d |
| witness-size |
3471 |
| witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174, sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i, bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174.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 (bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174, sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i, bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174.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 (bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174, sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i, bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174.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 (bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174, sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i, bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174.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 (bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174, sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i).
Found 3 witnesses for program sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i, bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174.json
| Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
 4e0a6e1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
9 |
2019-12-08T00:47:54+01:00 |
e55ccad |
|
6561285 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
9 |
2019-11-30T17:28:43+01:00 |
b3c9bfd |
|
b3c9bfd |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / svcomp20 |
15 |
2019-11-30T10:00:46+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174, sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i).
Found 10 witnesses for program sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i, bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174.json
| Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
|
031add7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
SMACK 1.9.3 |
3 |
2018-12-08T03:25:30 |
|
|
b1e0d87 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
15 |
2018-12-08T01:00:01+01:00 |
|
|
4ca8650 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
9 |
2018-12-10T20:13:56+01:00 |
5283198 |
|
9cbb913 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
9 |
2018-12-09T21:21:12+01:00 |
ed5470d |
|
b43d0d3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
9 |
2018-12-08T21:45:46+01:00 |
031add7 |
|
419127a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
10 |
2018-12-08T06:09:33+01:00 |
b1e0d87 |
|
3061674 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
9 |
2018-12-07T17:59:43+01:00 |
323284e |
|
07cadf0 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
9 |
2018-12-06T09:43:32+01:00 |
a092ffe |
|
ae6a8d8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
10 |
2018-12-06T09:06:31+01:00 |
013d7e3 |
|
013d7e3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
15 |
2018-12-05T13:45:46+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174, sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i).
Found 6 witnesses for program sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i, bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174.json
| Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
|
4ddc810 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26758M |
186 |
2017-11-30T18:42:39+01:00 |
|
|
acf892e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26725 |
112 |
2017-11-30T23:34:17+01:00 |
|
|
323284e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
skink |
3 |
2017-12-01T22:57 CET (sv-comp) |
|
|
5ed3f2a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.12-svcomp17 |
4 |
2017-11-02T13:16:17+05:30 |
|
|
53425d4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
9 |
2017-12-03T04:25:25+01:00 |
596030f |
|
f7d5496 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
9 |
2017-12-02T00:21:10+01:00 |
f32523a |
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174, sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i, bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174.json
| Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |