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/array-memsafety/cstrpbrk_unsafe_false-valid-deref.i |
programSHA |
3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee |
witnessName |
results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-memsafety.cstrpbrk_unsafe_false-valid-deref.i.files/witness.graphml |
witnessSHA |
a7893df3831ff45380d9d8eaa6401c7502b10fc44a2e52e72781d11509c69cff |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/a7893df3831ff45380d9d8eaa6401c7502b10fc44a2e52e72781d11509c69cff.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-05T13:50:50.960060 |
producer |
DepthK v3.0 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_6346dfd0-5842-44c2-82f5-e1657fe57075/sv-benchmarks/c/array-memsafety/cstrpbrk_unsafe_false-valid-deref.i |
programhash |
3d5e76e59f87104cc83de8acda77b849da7d1b09 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
witness-file |
witnessFileByHash/a7893df3831ff45380d9d8eaa6401c7502b10fc44a2e52e72781d11509c69cff.graphml |
witness-sha256 |
a7893df3831ff45380d9d8eaa6401c7502b10fc44a2e52e72781d11509c69cff |
witness-size |
4535 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee, sv-benchmarks/c/array-memsafety/cstrpbrk_unsafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/cstrpbrk_unsafe_false-valid-deref.i, 3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee.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 (3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee, sv-benchmarks/c/array-memsafety/cstrpbrk_unsafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/cstrpbrk_unsafe_false-valid-deref.i, 3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee.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 (3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee, sv-benchmarks/c/array-memsafety/cstrpbrk_unsafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/cstrpbrk_unsafe_false-valid-deref.i, 3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee.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 (3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee, sv-benchmarks/c/array-memsafety/cstrpbrk_unsafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/cstrpbrk_unsafe_false-valid-deref.i, 3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee.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 (3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee, sv-benchmarks/c/array-memsafety/cstrpbrk_unsafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/cstrpbrk_unsafe_false-valid-deref.i, 3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee.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 (3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee, sv-benchmarks/c/array-memsafety/cstrpbrk_unsafe_false-valid-deref.i).
Found 14 witnesses for program sv-benchmarks/c/array-memsafety/cstrpbrk_unsafe_false-valid-deref.i, 3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
1c50f0c |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
Symbiotic |
1 |
2018-12-08T18:00 CET (sv-comp) |
|
28c78f7 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-09T20:53:23+01:00 |
0af1543 |
15baaa7 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-08T04:56:56+01:00 |
be32aa1 |
8afd1eb |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
9 |
2018-12-07T05:34:28+01:00 |
|
a6e4ea1 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
9 |
2018-12-09T20:25:48+01:00 |
0500692 |
f6b63fd |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
9 |
2018-12-06T09:14:39+01:00 |
7251fb9 |
a6fca6c |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
9 |
2018-12-05T19:23:08+01:00 |
|
d57eeee |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
9 |
2018-12-07T09:12:54+01:00 |
06f232c |
38b07e6 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
SMACK 1.9.3 |
4 |
2018-12-08T11:29:45 |
|
499f917 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-09T20:38:41+01:00 |
3884ef4 |
f1a29e1 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
9 |
2018-12-08T22:11:30+01:00 |
38b07e6 |
bbd3ec5 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-06T10:17:48+01:00 |
a7893df |
f4add08 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
9 |
2018-12-08T23:43:34+01:00 |
1c50f0c |
f48f192 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
9 |
2018-12-07T01:19:14+01:00 |
4013c6b |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee, sv-benchmarks/c/array-memsafety/cstrpbrk_unsafe_false-valid-deref.i).
Found 9 witnesses for program sv-benchmarks/c/array-memsafety/cstrpbrk_unsafe_false-valid-deref.i, 3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
056bb54 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
Symbiotic |
1 |
2017-12-02T23:37 CET (sv-comp) |
|
1bbc757 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
violation_witness |
ESBMC 4.6.0 kind |
4 |
2017-12-02T10:56:13.137204 |
|
d0d13eb |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
violation_witness |
ESBMC 4.6.0 incr |
4 |
2017-12-01T23:29:07.841805 |
|
8df0081 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
violation_witness |
ESBMC 3.1 |
4 |
2017-12-01T09:33 CET (sv-comp) |
|
6dfafdb |
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 |
11 |
2017-12-03T06:53Z |
|
d0be66b |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
Kojak |
11 |
2017-12-03T04:23Z |
|
501fbab |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
CBMC |
8 |
2017-12-01T08:26 CET (sv-comp) |
|
e8284da |
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 |
11 |
2017-12-03T04:20Z |
|
ae5cc3b |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
Map2Check |
3 |
2017-12-01T23:54 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee, sv-benchmarks/c/array-memsafety/cstrpbrk_unsafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/cstrpbrk_unsafe_false-valid-deref.i, 3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/3bc4a6621eb5b4df3fba809a2a6648cd5fc9e3cd7e1cc4489a9c5730adf238ee.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |