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/memsafety-ext3/scopes4_true-valid-memsafety.c |
programSHA |
58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606 |
witnessName |
results-verified/utaipan.2018-12-08_1419.logfiles/sv-comp19_prop-memsafety.scopes4_true-valid-memsafety.c.files/witness.graphml |
witnessSHA |
f7ae297a4249a8e03ab40d059a5a1a8b370a9b68c6a5b83f29192a7fa781b783 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/f7ae297a4249a8e03ab40d059a5a1a8b370a9b68c6a5b83f29192a7fa781b783.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-09T18:36Z |
error-specification-length |
Key 'specification' longer than 100 characters. |
producer |
Taipan |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_fa4ebb92-bc92-4998-8c96-d075c236542e/sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c |
programhash |
87dcbb1d4539995e5aba39e6053775ca0fac811e |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) )
|
witness-file |
witnessFileByHash/f7ae297a4249a8e03ab40d059a5a1a8b370a9b68c6a5b83f29192a7fa781b783.graphml |
witness-sha256 |
f7ae297a4249a8e03ab40d059a5a1a8b370a9b68c6a5b83f29192a7fa781b783 |
witness-size |
6073 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606, sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c).
Found 15 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c, 58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
999f3eb |
Inspect |
|
valid-memsafety |
correctness_witness |
DIVINE 4 |
2 |
2023-12-18T10:32:58+01:00 |
|
1d304ce |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-29T23:10:48Z |
|
d313c5f |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-11-30T04:50:51+01:00 |
|
153e4ff |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
4 |
2023-12-03T23:10:58+01:00 |
|
df6a0f6 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-38892M |
5 |
2023-12-18T01:35:57+01:00 |
|
f17b780 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-05T11:33:31Z |
|
2320970 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-04T14:28:57Z |
|
188b2f2 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-01T20:26:09Z |
|
9a59bac |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 7.4.0 incr |
3 |
2023-12-01T14:10:34Z |
|
f0fb379 |
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 |
7 |
2023-12-02T11:22:11Z |
|
b61fefd |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
PredatorHP |
4 |
2023-11-30T08:25:30Z |
|
7832657 |
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-29T08:47:19Z |
|
f91c178 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
6 |
2023-12-01T01:14:52Z |
|
472dee6 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CBMC |
4 |
2023-12-17T11:20:28+01:00 |
|
b3e5b24 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
4 |
2023-12-18T18:44:48+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606, sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c).
Found 11 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c, 58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
d59c91c |
Inspect |
|
valid-memsafety |
correctness_witness |
DIVINE 4 |
2 |
2022-12-09T06:47:41+01:00 |
|
0e45839 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2 |
4 |
2022-12-10T14:48:01+01:00 |
|
f1957fa |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2.1-svn-1715bd67dc+ |
4 |
2022-12-12T01:44:43+01:00 |
|
9a14a5f |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-38892M |
5 |
2022-12-09T02:57:45+01:00 |
|
98aba79 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2022-12-08T20:46:34Z |
|
461e0d4 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 7.0.0 incr |
3 |
2022-12-18T20:12:28Z |
|
ee4e3c5 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 6.8.0 incr |
3 |
2022-12-25T08:29:41Z |
|
ec57e02 |
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 |
7 |
2022-12-14T06:26:37Z |
|
fcaa524 |
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 |
2022-12-11T10:55:59Z |
|
a87bdf4 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CBMC |
4 |
2022-12-08T05:30:52+01:00 |
|
e99be05 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
4 |
2022-12-10T01:41:46+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606, sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c).
Found 11 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c, 58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
3b867ad |
Inspect |
|
valid-memsafety |
correctness_witness |
DIVINE 4 |
2 |
2021-12-07T09:17:53+01:00 |
|
9097bde |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.1 |
4 |
2021-12-05T18:52:29+01:00 |
|
a1ba210 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-eda176372c+ |
4 |
2021-12-09T10:31:28+01:00 |
|
d6b04b4 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-38892M |
5 |
2021-12-07T01:55:33+01:00 |
|
bd52bdd |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 6.8.0 incr |
3 |
2021-12-08T05:32:15Z |
|
da711e3 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 2.0.1-svn-fe6f522dd3+ |
4 |
2021-12-08T18:18:18+01:00 |
|
c668db2 |
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 |
7 |
2021-12-10T05:52:34Z |
|
a25d753 |
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 |
7 |
2021-12-10T09:03:59Z |
|
3a9db48 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CBMC |
4 |
2021-12-06T07:40:38+01:00 |
|
66887f9 |
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 |
7 |
2021-12-06T19:58:51Z |
|
de4bce5 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
SESL |
2 |
2021-12-06T11:30:53+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '21
Trying to find witnesses for program (58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606, sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c).
Found 3 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c, 58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
6a2d4c3 |
Inspect |
|
valid-memsafety |
correctness_witness |
DIVINE 4 |
2 |
2020-12-06T17:40:48+01:00 |
|
20d5d21 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0 |
4 |
2020-12-05T16:54:01+01:00 |
|
a955d8b |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-eda176372c+ |
4 |
2020-12-07T22:29:11+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '20
Trying to find witnesses for program (58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606, sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c).
Found 2 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c, 58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
ab78acb |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.9 |
4 |
2019-11-29T21:26:55+01:00 |
|
b14861d |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ |
4 |
2019-12-01T17:58:15+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606, sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c).
Found 3 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c, 58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
48c7281 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
1 |
2018-12-08T08:03 CET (sv-comp) |
|
69bccf4 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
4 |
2018-12-07T10:42:29+01:00 |
|
fe0c781 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
4 |
2018-12-05T14:47:08+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606, sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c).
Found 0 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c, 58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606.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 (58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606, sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c).
Found 0 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c, 58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |