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/parport_true-unreach-call.i.cil.c |
programSHA |
91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97 |
witnessName |
results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-reachsafety.parport_true-unreach-call.i.cil.c.files/witness.graphml |
witnessSHA |
7febe63890f4a5fe8780831befa41d2526100e0255f9d7d124b6c9137abac3a2 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/7febe63890f4a5fe8780831befa41d2526100e0255f9d7d124b6c9137abac3a2.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-06T03:35:01.075824 |
producer |
DepthK v3.0 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_82b91a26-9812-43b4-8f4e-231451a3d0b5/sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c |
programhash |
c382c054908dd436240a631a5e6d7113fd867a7b |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/7febe63890f4a5fe8780831befa41d2526100e0255f9d7d124b6c9137abac3a2.graphml |
witness-sha256 |
7febe63890f4a5fe8780831befa41d2526100e0255f9d7d124b6c9137abac3a2 |
witness-size |
3468 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97, sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c).
Found 0 witnesses for program sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c, 91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97.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 (91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97, sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c).
Found 0 witnesses for program sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c, 91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97.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 (91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97, sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c).
Found 0 witnesses for program sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c, 91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97.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 (91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97, sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c).
Found 0 witnesses for program sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c, 91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97.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 (91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97, sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c).
Found 0 witnesses for program sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c, 91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97.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 (91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97, sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c).
Found 8 witnesses for program sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c, 91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
056ce27 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
SMACK 1.9.3 |
3 |
2018-12-08T05:56:53 |
|
70099bc |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
599 |
2018-12-08T01:52:51+01:00 |
|
51ddfb0 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
599 |
2018-12-08T21:26:20+01:00 |
056ce27 |
9c65e32 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
599 |
2018-12-08T06:49:02+01:00 |
70099bc |
98d1711 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
599 |
2018-12-08T03:22:07+01:00 |
a53e09c |
12c13d9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
599 |
2018-12-06T09:28:51+01:00 |
7febe63 |
1e7a438 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
599 |
2018-12-06T08:45:32+01:00 |
6d00857 |
6d00857 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
599 |
2018-12-06T04:00:48+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97, sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c).
Found 0 witnesses for program sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c, 91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97.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 (91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97, sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c).
Found 0 witnesses for program sv-benchmarks/c/ntdrivers/parport_true-unreach-call.i.cil.c, 91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/91e41fbf2c68965218866787abb6ba3ebe0a2d8289f82e8ce043d5008240fa97.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |