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/count_down_unsafe_false-valid-deref.i |
programSHA |
e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb |
witnessName |
results-verified/ukojak.2018-12-08_1104.logfiles/sv-comp19_prop-memsafety.count_down_unsafe_false-valid-deref.i.files/witness.graphml |
witnessSHA |
7e1aff68f422a5b297204be9a7bf966be5705da25010010a31afb1f1a44d33d2 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/7e1aff68f422a5b297204be9a7bf966be5705da25010010a31afb1f1a44d33d2.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-09T04:06Z |
error-specification-length |
Key 'specification' longer than 100 characters. |
producer |
Kojak |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_7611c890-ca39-497d-a951-8631204f1030/sv-benchmarks/c/array-memsafety/count_down_unsafe_false-valid-deref.i |
programhash |
71c9f2b0d8bf95458c9b099304dfb78f8cadcf0a |
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/7e1aff68f422a5b297204be9a7bf966be5705da25010010a31afb1f1a44d33d2.graphml |
witness-sha256 |
7e1aff68f422a5b297204be9a7bf966be5705da25010010a31afb1f1a44d33d2 |
witness-size |
6878 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb, sv-benchmarks/c/array-memsafety/count_down_unsafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/count_down_unsafe_false-valid-deref.i, e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb.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 (e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb, sv-benchmarks/c/array-memsafety/count_down_unsafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/count_down_unsafe_false-valid-deref.i, e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb.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 (e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb, sv-benchmarks/c/array-memsafety/count_down_unsafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/count_down_unsafe_false-valid-deref.i, e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb.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 (e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb, sv-benchmarks/c/array-memsafety/count_down_unsafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/count_down_unsafe_false-valid-deref.i, e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb.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 (e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb, sv-benchmarks/c/array-memsafety/count_down_unsafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/count_down_unsafe_false-valid-deref.i, e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb.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 (e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb, sv-benchmarks/c/array-memsafety/count_down_unsafe_false-valid-deref.i).
Found 14 witnesses for program sv-benchmarks/c/array-memsafety/count_down_unsafe_false-valid-deref.i, e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
e8face3 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
Symbiotic |
2 |
2018-12-08T09:36 CET (sv-comp) |
|
1dd14b4 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-09T20:38:04+01:00 |
28a51cf |
bb0b8f1 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-08T22:09:54+01:00 |
1dfa183 |
d010c4b |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
6 |
2018-12-06T10:17:25+01:00 |
d3f4480 |
84e9549 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-09T20:28:44+01:00 |
7e1aff6 |
2fc9a65 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-05T22:33:27+01:00 |
|
2bb66d1 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-06T09:17:30+01:00 |
1ce6692 |
626d420 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-07T09:22:20+01:00 |
5da9325 |
1dfa183 |
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-07T20:19:50 |
|
7f7d860 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-09T20:53:23+01:00 |
2e27efb |
8daac56 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-08T23:41:57+01:00 |
e8face3 |
e863507 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-08T05:03:48+01:00 |
5102311 |
820359f |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-07T01:17:05+01:00 |
9c547a2 |
92204e1 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
8 |
2018-12-08T02:52:28+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb, sv-benchmarks/c/array-memsafety/count_down_unsafe_false-valid-deref.i).
Found 9 witnesses for program sv-benchmarks/c/array-memsafety/count_down_unsafe_false-valid-deref.i, e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
ec09287 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
Symbiotic |
2 |
2017-12-03T00:12 CET (sv-comp) |
|
e6ad731 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
violation_witness |
ESBMC 4.6.0 kind |
4 |
2017-12-02T12:00:08.901539 |
|
41eee8b |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
violation_witness |
ESBMC 4.6.0 incr |
4 |
2017-12-01T23:14:18.628589 |
|
f1ccae6 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
violation_witness |
ESBMC 3.1 |
5 |
2017-12-01T09:21 CET (sv-comp) |
|
ee62e35 |
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 |
7 |
2017-12-03T06:53Z |
|
506b3f7 |
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 |
6 |
2017-12-03T04:26Z |
|
4dd1d2c |
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 |
5 |
2017-12-01T08:21 CET (sv-comp) |
|
6c8f1c1 |
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 |
6 |
2017-12-03T04:14Z |
|
ed18f87 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
Map2Check |
3 |
2017-12-01T23:22 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb, sv-benchmarks/c/array-memsafety/count_down_unsafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/count_down_unsafe_false-valid-deref.i, e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/e51193982835fc13b2dad5d1ca659a8d47d4025781b6f4a74731a3996051f3cb.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |