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-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i |
| programSHA |
7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf |
| witnessName |
results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-termination.openbsd_cmemchr-alloca_true-termination.c.i.files/witness.graphml |
| witnessSHA |
2c358f15b2f113ad15b9aadd12b6affc4289aed728ed634136cda7b8a87d6722 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/2c358f15b2f113ad15b9aadd12b6affc4289aed728ed634136cda7b8a87d6722.json
| Key |
Value |
| architecture |
32bit |
| creationtime |
2018-12-05T17:32:51.113762 |
| producer |
DepthK v3.0 |
| programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_3e08cdde-b40a-4bca-9314-39f82213107f/sv-benchmarks/c/termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i |
| programhash |
41c98898a531fb0ee2da225b716afd5dc80c24b1 |
| sourcecodelang |
C |
| specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
| witness-file |
witnessFileByHash/2c358f15b2f113ad15b9aadd12b6affc4289aed728ed634136cda7b8a87d6722.graphml |
| witness-sha256 |
2c358f15b2f113ad15b9aadd12b6affc4289aed728ed634136cda7b8a87d6722 |
| witness-size |
3494 |
| witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf, sv-benchmarks/c/termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i).
Found 12 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i, 7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf.json
| Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
 bca378a |
Inspect |
|
valid-memsafety |
violation_witness |
DIVINE 4 |
2 |
2023-12-18T09:08:21+01:00 |
|
|
754fcbd |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
3 |
2023-12-17T00:48:47Z |
|
|
c3e331c |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-18T12:07:22+01:00 |
bca378a |
|
46ef3da |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-11-30T06:19:46+01:00 |
|
|
806386c |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
7 |
2023-12-03T23:01:47+01:00 |
|
|
89a7843 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
7 |
2023-12-19T00:24:17+01:00 |
|
|
eb32a8c |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-38892M |
10 |
2023-12-18T01:33:38+01:00 |
|
|
aa709cd |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Taipan |
13 |
2023-12-02T18:17:08Z |
|
|
2d08a93 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Mopsa (v1.0~pre2) |
3 |
2023-11-29T12:27:37Z |
|
|
ae769b2 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Kojak |
13 |
2023-12-03T01:03:38Z |
|
|
7a33c59 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Automizer |
12 |
2023-11-29T03:20:37Z |
|
|
88da430 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 2.0 |
7 |
2023-12-19T11:05:04+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf, sv-benchmarks/c/termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i).
Found 10 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i, 7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf.json
| Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
|
d9a1f08 |
Inspect |
|
valid-memsafety |
violation_witness |
DIVINE 4 |
2 |
2022-12-09T06:26:02+01:00 |
|
|
c6bd87f |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
3 |
2022-12-25T10:16:19Z |
|
|
4030b75 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2 |
7 |
2023-01-28T14:13:32+01:00 |
d9a1f08 |
|
44d2cc0 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2 |
7 |
2022-12-10T15:34:37+01:00 |
|
|
2984898 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2.1-svn-1715bd67dc+ |
7 |
2022-12-11T21:45:39+01:00 |
|
|
9b48583 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0 |
7 |
2022-12-11T05:44:37+01:00 |
|
|
eab3cac |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
7 |
2022-12-10T02:35:40+01:00 |
|
|
b77160f |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-38892M |
10 |
2022-12-09T02:26:51+01:00 |
|
|
5254c74 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Taipan |
11 |
2022-12-14T05:17:05Z |
|
|
5240e82 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Automizer |
11 |
2022-12-13T17:03:02Z |
|
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf, sv-benchmarks/c/termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i).
Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i, 7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf.json
| Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
|
749e8fc |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2021-12-10T18:23:35 |
|
Available Results for the Program from Witness Store SV-COMP '21
Trying to find witnesses for program (7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf, sv-benchmarks/c/termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i).
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i, 7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf.json
| Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
|
df5ab2d |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2020-12-11T19:34:14 |
|
|
f317b8c |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2020-12-09T01:58:42 |
|
Available Results for the Program from Witness Store SV-COMP '20
Trying to find witnesses for program (7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf, sv-benchmarks/c/termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i).
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i, 7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf.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 (7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf, sv-benchmarks/c/termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i).
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i, 7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf.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 (7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf, sv-benchmarks/c/termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i).
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i, 7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf.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 (7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf, sv-benchmarks/c/termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i).
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cmemchr-alloca_true-termination.c.i, 7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/7f0d11c5f3d4193dc8b87cb3dbae552e2a558805da02a0660bf5cf3361799dbf.json
| Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |