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/heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i |
programSHA |
43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea |
witnessName |
results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.dll_of_dll_true-unreach-call_true-valid-memsafety.i.files/witness.graphml |
witnessSHA |
4a512cf95cce30ad6320985a95168339daf73c1f360dbccdb41b05fabcb045dd |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/4a512cf95cce30ad6320985a95168339daf73c1f360dbccdb41b05fabcb045dd.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-01T03:29:29+01:00 |
producer |
CPAchecker 1.6.1-svn 26773 |
program-sha256 |
43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea |
programfile |
../../sv-benchmarks/c/heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i |
programhash |
30912d79507d112674315a135c457bdb2fa6a53f |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/4a512cf95cce30ad6320985a95168339daf73c1f360dbccdb41b05fabcb045dd.graphml |
witness-sha256 |
4a512cf95cce30ad6320985a95168339daf73c1f360dbccdb41b05fabcb045dd |
witness-size |
18627 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea, sv-benchmarks/c/heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i).
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i, 43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea.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 (43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea, sv-benchmarks/c/heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i).
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i, 43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea.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 (43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea, sv-benchmarks/c/heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i).
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i, 43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea.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 (43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea, sv-benchmarks/c/heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i).
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i, 43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea.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 (43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea, sv-benchmarks/c/heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i).
Found 7 witnesses for program sv-benchmarks/c/heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i, 43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
6697f79 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.9 |
41 |
2019-11-30T13:52:50+01:00 |
|
2fe8033 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ |
41 |
2019-12-01T19:00:40+01:00 |
|
37fd298 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
18 |
2019-12-11T20:17:27+01:00 |
b52ecd2 |
d704923 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
18 |
2019-11-30T16:40:28+01:00 |
6480856 |
6480856 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
18 |
2019-11-30T14:36:08+01:00 |
|
b52ecd2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
18 |
2019-12-01T00:20:11+01:00 |
|
fb93638 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
41 |
2019-12-07T23:47:11+01:00 |
a886ed3 |
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea, sv-benchmarks/c/heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i).
Found 4 witnesses for program sv-benchmarks/c/heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i, 43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
ec1137c |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
41 |
2018-12-08T03:45:22+01:00 |
|
8627078 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
41 |
2018-12-05T16:56:36+01:00 |
|
637a76a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
39 |
2018-12-08T03:47:41+01:00 |
|
413017c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
42 |
2018-12-08T05:24:30+01:00 |
637a76a |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea, sv-benchmarks/c/heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i).
Found 4 witnesses for program sv-benchmarks/c/heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i, 43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
4a512cf |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
19 |
2017-12-01T03:29:29+01:00 |
|
8446651 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker (unknown version) |
20 |
2017-12-02T06:06:37+01:00 |
|
0380dc6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
PredatorHP |
4 |
2017-12-01T20:24 CET (sv-comp) |
|
c1f4dd7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
42 |
2017-12-01T21:07:51+01:00 |
b4e5a76 |
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea, sv-benchmarks/c/heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i).
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i, 43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/43951ed18ce7424bb8088534386736755224eaa5d5de40b03ec5d85519443dea.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |