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/termination-libowfat/dirname_true-termination.c.i |
| programSHA |
c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754 |
| witnessName |
results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-termination.dirname_true-termination.c.i.files/witness.graphml |
| witnessSHA |
fbdd8a1a9ac7f7725d69dbc834bd1282e72e168c607de054a63f0b0df5497710 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/fbdd8a1a9ac7f7725d69dbc834bd1282e72e168c607de054a63f0b0df5497710.json
| Key |
Value |
| architecture |
32bit |
| creationtime |
2018-12-06T01:48:43.957381 |
| producer |
DepthK v3.0 |
| programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_62e217b3-a147-4d27-9e85-3b2eea9a3f94/sv-benchmarks/c/termination-libowfat/dirname_true-termination.c.i |
| programhash |
d734a045af079c429b3228f88cbcf1ebcca0a1be |
| sourcecodelang |
C |
| specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
| witness-file |
witnessFileByHash/fbdd8a1a9ac7f7725d69dbc834bd1282e72e168c607de054a63f0b0df5497710.graphml |
| witness-sha256 |
fbdd8a1a9ac7f7725d69dbc834bd1282e72e168c607de054a63f0b0df5497710 |
| witness-size |
3474 |
| witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754, sv-benchmarks/c/termination-libowfat/dirname_true-termination.c.i).
Found 12 witnesses for program sv-benchmarks/c/termination-libowfat/dirname_true-termination.c.i, c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754.json
| Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
 f91210a |
Inspect |
|
valid-memsafety |
violation_witness |
DIVINE 4 |
2 |
2023-12-18T09:58:13+01:00 |
|
|
20e9e6c |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.3 |
12 |
2023-12-18T12:08:02+01:00 |
f91210a |
|
bbbc298 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.3 |
12 |
2023-12-04T12:13:00+01:00 |
78a8a2e |
|
063ffc2 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.3 |
12 |
2023-12-01T18:29:40+01:00 |
e40a0eb |
|
29e096b |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.3 |
12 |
2023-11-30T06:17:08+01:00 |
|
|
7969222 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.3 |
12 |
2023-11-29T08:33:44+01:00 |
bcc3ea7 |
|
90b00f8 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
12 |
2023-12-03T22:20:34+01:00 |
|
|
b5f7d9d |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
12 |
2023-12-18T17:59:42+01:00 |
|
|
b865ba1 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-38892M |
16 |
2023-12-18T01:33:35+01:00 |
|
|
e40a0eb |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
violation_witness |
ESBMC 7.4.0 incr |
6 |
2023-12-01T13:27:37Z |
|
|
78a8a2e |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
Taipan |
9 |
2023-12-02T15:46:10Z |
|
|
bcc3ea7 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
Automizer |
9 |
2023-11-29T00:23:33Z |
|
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754, sv-benchmarks/c/termination-libowfat/dirname_true-termination.c.i).
Found 14 witnesses for program sv-benchmarks/c/termination-libowfat/dirname_true-termination.c.i, c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754.json
| Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
|
b6a8f75 |
Inspect |
|
valid-memsafety |
violation_witness |
DIVINE 4 |
2 |
2022-12-09T06:30:01+01:00 |
|
|
a19ea94 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2 |
12 |
2023-01-29T10:45:23+01:00 |
cd209d8 |
|
217df12 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2 |
12 |
2023-01-29T06:53:48+01:00 |
8a485f6 |
|
099c324 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2 |
12 |
2023-01-29T04:19:22+01:00 |
672f674 |
|
abf0e60 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2 |
12 |
2023-01-28T15:43:43+01:00 |
ec682fb |
|
f9aaa94 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2 |
12 |
2023-01-28T14:20:30+01:00 |
b6a8f75 |
|
b6bf5f2 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2 |
12 |
2022-12-10T17:35:46+01:00 |
|
|
83b5a37 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2.1-svn-1715bd67dc+ |
12 |
2022-12-11T21:51:52+01:00 |
|
|
8973e25 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.1 |
12 |
2022-12-25T11:28:14+01:00 |
|
|
9f18472 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-38892M |
16 |
2022-12-09T03:12:00+01:00 |
|
|
ec682fb |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
violation_witness |
ESBMC 7.0.0 incr |
5 |
2022-12-19T00:03:41Z |
|
|
cd209d8 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
Taipan |
9 |
2022-12-14T13:09:04Z |
|
|
8a485f6 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
Automizer |
9 |
2022-12-13T19:30:28Z |
|
|
22305ae |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
12 |
2022-12-10T04:40:11+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754, sv-benchmarks/c/termination-libowfat/dirname_true-termination.c.i).
Found 1 witnesses for program sv-benchmarks/c/termination-libowfat/dirname_true-termination.c.i, c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754.json
| Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
|
1eac147 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2021-12-10T18:39:14 |
|
Available Results for the Program from Witness Store SV-COMP '21
Trying to find witnesses for program (c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754, sv-benchmarks/c/termination-libowfat/dirname_true-termination.c.i).
Found 2 witnesses for program sv-benchmarks/c/termination-libowfat/dirname_true-termination.c.i, c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754.json
| Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
|
1a367a2 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2020-12-11T17:02:39 |
|
|
b539531 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2020-12-08T23:46:57 |
|
Available Results for the Program from Witness Store SV-COMP '20
Trying to find witnesses for program (c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754, sv-benchmarks/c/termination-libowfat/dirname_true-termination.c.i).
Found 0 witnesses for program sv-benchmarks/c/termination-libowfat/dirname_true-termination.c.i, c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754.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 (c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754, sv-benchmarks/c/termination-libowfat/dirname_true-termination.c.i).
Found 0 witnesses for program sv-benchmarks/c/termination-libowfat/dirname_true-termination.c.i, c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754.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 '18
Trying to find witnesses for program (c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754, sv-benchmarks/c/termination-libowfat/dirname_true-termination.c.i).
Found 0 witnesses for program sv-benchmarks/c/termination-libowfat/dirname_true-termination.c.i, c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754.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 (c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754, sv-benchmarks/c/termination-libowfat/dirname_true-termination.c.i).
Found 0 witnesses for program sv-benchmarks/c/termination-libowfat/dirname_true-termination.c.i, c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/c17dc684f0856c2cb34d9c0f310a5ac71ddc07f596d7c8c46ee2d12464efc754.json
| Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |