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/ntdrivers/diskperf_false-unreach-call.i.cil.c |
programSHA |
2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79 |
witnessName |
results-verified/esbmc-kind.2018-12-06_1103.logfiles/sv-comp19_prop-reachsafety.diskperf_false-unreach-call.i.cil.c.files/witness.graphml |
witnessSHA |
8b2d5772ce506c60e91807443f1b0f90abe4f34fbfb99df40decd80793337214 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/8b2d5772ce506c60e91807443f1b0f90abe4f34fbfb99df40decd80793337214.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-07T13:37:13.951878 |
producer |
ESBMC 6.0.0 kind |
programfile |
../../sv-benchmarks/c/ntdrivers/diskperf_false-unreach-call.i.cil.c |
programhash |
f1801b43b2944393728b18bd2d618b5a8c03e37d |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/8b2d5772ce506c60e91807443f1b0f90abe4f34fbfb99df40decd80793337214.graphml |
witness-sha256 |
8b2d5772ce506c60e91807443f1b0f90abe4f34fbfb99df40decd80793337214 |
witness-size |
4826 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79, sv-benchmarks/c/ntdrivers/diskperf_false-unreach-call.i.cil.c).
Found 0 witnesses for program sv-benchmarks/c/ntdrivers/diskperf_false-unreach-call.i.cil.c, 2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79.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 (2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79, sv-benchmarks/c/ntdrivers/diskperf_false-unreach-call.i.cil.c).
Found 0 witnesses for program sv-benchmarks/c/ntdrivers/diskperf_false-unreach-call.i.cil.c, 2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79.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 (2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79, sv-benchmarks/c/ntdrivers/diskperf_false-unreach-call.i.cil.c).
Found 0 witnesses for program sv-benchmarks/c/ntdrivers/diskperf_false-unreach-call.i.cil.c, 2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79.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 (2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79, sv-benchmarks/c/ntdrivers/diskperf_false-unreach-call.i.cil.c).
Found 0 witnesses for program sv-benchmarks/c/ntdrivers/diskperf_false-unreach-call.i.cil.c, 2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79.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 (2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79, sv-benchmarks/c/ntdrivers/diskperf_false-unreach-call.i.cil.c).
Found 0 witnesses for program sv-benchmarks/c/ntdrivers/diskperf_false-unreach-call.i.cil.c, 2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79.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 '19
Trying to find witnesses for program (2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79, sv-benchmarks/c/ntdrivers/diskperf_false-unreach-call.i.cil.c).
Found 14 witnesses for program sv-benchmarks/c/ntdrivers/diskperf_false-unreach-call.i.cil.c, 2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
f204c4c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
12 |
2018-12-08T05:00:56 |
|
bc43047 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Pinaka |
23 |
2018-12-07T09:41 CET (sv-comp) |
|
b23d5d9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7 |
37 |
2018-12-10T19:03:06+01:00 |
|
f7f7f27 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
26 |
2018-12-07T13:25:11+01:00 |
|
932ce16 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
27 |
2018-12-09T17:48:14+01:00 |
465692d |
a706350 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
28 |
2018-12-08T22:07:57+01:00 |
f204c4c |
a1e6a8a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
28 |
2018-12-08T08:20:30+01:00 |
f7f7f27 |
59f6b75 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
27 |
2018-12-06T09:49:03+01:00 |
ed7c4d2 |
ed7c4d2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
25 |
2018-12-05T06:21:56+01:00 |
|
63ec43b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
127 |
2018-12-10T20:36:21+01:00 |
b23d5d9 |
1dd13e4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
127 |
2018-12-08T04:56:08+01:00 |
8b2d577 |
4f19052 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
127 |
2018-12-06T10:17:33+01:00 |
8dcc177 |
baf9f1a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
127 |
2018-12-06T09:21:23+01:00 |
95b787e |
8493b24 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
127 |
2018-12-06T09:16:46+01:00 |
47cb2b4 |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79, sv-benchmarks/c/ntdrivers/diskperf_false-unreach-call.i.cil.c).
Found 0 witnesses for program sv-benchmarks/c/ntdrivers/diskperf_false-unreach-call.i.cil.c, 2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79.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 '17
Trying to find witnesses for program (2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79, sv-benchmarks/c/ntdrivers/diskperf_false-unreach-call.i.cil.c).
Found 0 witnesses for program sv-benchmarks/c/ntdrivers/diskperf_false-unreach-call.i.cil.c, 2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/2b82b923aa98423bab3b8083731bc84d5aec63c9cccd01ed2ac7d88c9b110a79.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |