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/tree_false-valid-deref.i |
programSHA |
edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b |
witnessName |
results-verified/ukojak.2018-12-08_1104.logfiles/sv-comp19_prop-memsafety.tree_false-valid-deref.i.files/witness.graphml |
witnessSHA |
55b0d4b3594a45f0e970d51f6f6cebf17bddb116f36761b77e3b64c003754a49 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/55b0d4b3594a45f0e970d51f6f6cebf17bddb116f36761b77e3b64c003754a49.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-09T15:10Z |
error-specification-length |
Key 'specification' longer than 100 characters. |
producer |
Kojak |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_42ddaa0f-c364-407d-a2d0-3e16d9a45967/sv-benchmarks/c/heap-manipulation/tree_false-valid-deref.i |
programhash |
044ef52817dc7382960a6f0241b98ee90ba1b40d |
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/55b0d4b3594a45f0e970d51f6f6cebf17bddb116f36761b77e3b64c003754a49.graphml |
witness-sha256 |
55b0d4b3594a45f0e970d51f6f6cebf17bddb116f36761b77e3b64c003754a49 |
witness-size |
4285 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b, sv-benchmarks/c/heap-manipulation/tree_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/tree_false-valid-deref.i, edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b.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 (edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b, sv-benchmarks/c/heap-manipulation/tree_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/tree_false-valid-deref.i, edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b.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 (edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b, sv-benchmarks/c/heap-manipulation/tree_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/tree_false-valid-deref.i, edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b.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 (edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b, sv-benchmarks/c/heap-manipulation/tree_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/tree_false-valid-deref.i, edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b.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 (edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b, sv-benchmarks/c/heap-manipulation/tree_false-valid-deref.i).
Found 14 witnesses for program sv-benchmarks/c/heap-manipulation/tree_false-valid-deref.i, edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
c738f33 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
Symbiotic |
1 |
2019-12-01 06:01:55 |
|
462fc34 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
CPAchecker 1.9 |
5 |
2019-12-11T21:09:43+01:00 |
c738f33 |
39b9c7d |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
CPAchecker 1.9 |
5 |
2019-12-08T00:26:07+01:00 |
fa086b7 |
308784a |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
CPAchecker 1.9 |
5 |
2019-12-08T00:06:12+01:00 |
3c7a805 |
ca19e48 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
CPAchecker 1.9 |
5 |
2019-12-06T02:38:13+01:00 |
71ab82a |
eb24de1 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.9 |
17 |
2019-12-11T21:55:47+01:00 |
0b386c4 |
8c60735 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.9 |
17 |
2019-12-03T08:10:56+01:00 |
52f41f5 |
0b386c4 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ |
17 |
2019-12-01T07:37:10+01:00 |
|
6ba7667 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
violation_witness |
CPAchecker 1.9 |
5 |
2019-12-07T21:15:08+01:00 |
d857f43 |
816d63c |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.9 |
17 |
2019-12-11T20:55:20+01:00 |
606b7eb |
52f41f5 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.9 |
17 |
2019-11-29T18:55:04+01:00 |
|
f2be252 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
CPAchecker 1.9 |
5 |
2019-12-11T21:54:11+01:00 |
5816985 |
ef7e139 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
CPAchecker 1.9 |
5 |
2019-12-05T20:20:40+01:00 |
1a20115 |
5995ffb |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
CPAchecker 1.9 |
5 |
2019-12-05T19:34:38+01:00 |
3bf63ce |
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b, sv-benchmarks/c/heap-manipulation/tree_false-valid-deref.i).
Found 16 witnesses for program sv-benchmarks/c/heap-manipulation/tree_false-valid-deref.i, edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
8c33e59 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
Symbiotic |
1 |
2018-12-08T14:13 CET (sv-comp) |
|
9b5f809 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-09T20:53:15+01:00 |
1367de8 |
b437299 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-08T22:10:11+01:00 |
c77001b |
900b2e3 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-08T03:36:51+01:00 |
97472a2 |
f1b2778 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-06T09:41:50+01:00 |
4ffd665 |
7a89f9e |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-06T09:17:47+01:00 |
268b65d |
115f865 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-09T20:38:32+01:00 |
c025640 |
087be70 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-07T09:16:27+01:00 |
f2fa841 |
01988bc |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
17 |
2018-12-06T20:15:55+01:00 |
|
c77001b |
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 |
3 |
2018-12-08T12:04:37 |
|
761b89c |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-09T20:32:31+01:00 |
55b0d4b |
690e90c |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-08T23:43:34+01:00 |
8c33e59 |
5ca01e7 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-08T05:05:33+01:00 |
641f6a0 |
9e8f25d |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-07T01:18:21+01:00 |
0504809 |
642f127 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-06T10:19:52+01:00 |
d30ee2c |
b4a1889 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
17 |
2018-12-06T05:18:07+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b, sv-benchmarks/c/heap-manipulation/tree_false-valid-deref.i).
Found 12 witnesses for program sv-benchmarks/c/heap-manipulation/tree_false-valid-deref.i, edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
e8589a3 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
Symbiotic |
1 |
2017-12-02T23:10 CET (sv-comp) |
|
bcf12f9 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
violation_witness |
ESBMC 4.6.0 kind |
4 |
2017-12-02T11:42:48.043756 |
|
fcdfc59 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
violation_witness |
ESBMC 4.6.0 incr |
4 |
2017-12-01T23:49:05.732402 |
|
b031533 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
violation_witness |
ESBMC 3.1 |
4 |
2017-12-01T09:21 CET (sv-comp) |
|
7efe606 |
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 |
5 |
2017-12-03T06:53Z |
|
78161d7 |
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 |
5 |
2017-12-03T04:22Z |
|
681d260 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
Forester |
4 |
2017-12-01T19:49 CET (sv-comp) |
|
930dc08 |
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 |
4 |
2017-12-01T08:25 CET (sv-comp) |
|
5cfa9f8 |
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 |
5 |
2017-12-03T03:46Z |
|
83db59f |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
2LS |
4 |
2017-12-01T08:19 CET (sv-comp) |
|
f2fa841 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
PredatorHP |
4 |
2017-12-01T22:13 CET (sv-comp) |
|
2bcca0e |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
Map2Check |
2 |
2017-12-01T23:55 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b, sv-benchmarks/c/heap-manipulation/tree_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/tree_false-valid-deref.i, edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/edf2325de73bf0b2dad984f093abe5a5226714f445037111e456cd46045f6b2b.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |