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 |
../../../comp/sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i |
programSHA |
bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174 |
witnessName |
results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.max20_true-unreach-call.i.files/witness.graphml |
witnessSHA |
5ed3f2a2ae2bb72705ea217c81cc1d21be12922e040fd47c6934f0a16e0b7459 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/5ed3f2a2ae2bb72705ea217c81cc1d21be12922e040fd47c6934f0a16e0b7459.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-11-02T13:16:17+05:30 |
producer |
CPAchecker 1.6.12-svcomp17 |
program-sha256 |
bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174 |
programfile |
/home/benchexec/ar_abs_temp/max20_true_unreach_call.c |
programhash |
67d74bcd4ddf537770c7e039af1f9d86f962eaff |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/5ed3f2a2ae2bb72705ea217c81cc1d21be12922e040fd47c6934f0a16e0b7459.graphml |
witness-sha256 |
5ed3f2a2ae2bb72705ea217c81cc1d21be12922e040fd47c6934f0a16e0b7459 |
witness-size |
3745 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (bac595bb3f2bf2fb48c3d8155448e8d9b24acb00dcbd43f0524b28f7e4fc0174, ../../../comp/sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i).
Found 0 witnesses for program ../../../comp/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, ../../../comp/sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i).
Found 0 witnesses for program ../../../comp/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, ../../../comp/sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i).
Found 0 witnesses for program ../../../comp/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, ../../../comp/sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i).
Found 0 witnesses for program ../../../comp/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, ../../../comp/sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i).
Found 3 witnesses for program ../../../comp/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, ../../../comp/sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i).
Found 10 witnesses for program ../../../comp/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, ../../../comp/sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i).
Found 6 witnesses for program ../../../comp/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, ../../../comp/sv-benchmarks/c/reducercommutativity/max20_true-unreach-call.i).
Found 0 witnesses for program ../../../comp/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 |