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/bubblesort_unsafe_false-valid-deref.i |
programSHA |
34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7 |
witnessName |
results-verified/esbmc-kind.2018-12-06_1103.logfiles/sv-comp19_prop-memsafety.bubblesort_unsafe_false-valid-deref.i.files/witness.graphml |
witnessSHA |
48813af0dc3a1c8d48c3d5bcfce79b1ee47464c9690ab711a2f23d5155e456ba |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/48813af0dc3a1c8d48c3d5bcfce79b1ee47464c9690ab711a2f23d5155e456ba.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-07T18:10:15.706208 |
producer |
ESBMC 6.0.0 kind |
programfile |
../../sv-benchmarks/c/array-memsafety/bubblesort_unsafe_false-valid-deref.i |
programhash |
d947ac2f4314b6371797f06202127d0425ea9bb5 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
witness-file |
witnessFileByHash/48813af0dc3a1c8d48c3d5bcfce79b1ee47464c9690ab711a2f23d5155e456ba.graphml |
witness-sha256 |
48813af0dc3a1c8d48c3d5bcfce79b1ee47464c9690ab711a2f23d5155e456ba |
witness-size |
4007 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7, sv-benchmarks/c/array-memsafety/bubblesort_unsafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/bubblesort_unsafe_false-valid-deref.i, 34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7.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 (34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7, sv-benchmarks/c/array-memsafety/bubblesort_unsafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/bubblesort_unsafe_false-valid-deref.i, 34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7.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 (34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7, sv-benchmarks/c/array-memsafety/bubblesort_unsafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/bubblesort_unsafe_false-valid-deref.i, 34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7.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 (34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7, sv-benchmarks/c/array-memsafety/bubblesort_unsafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/bubblesort_unsafe_false-valid-deref.i, 34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7.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 (34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7, sv-benchmarks/c/array-memsafety/bubblesort_unsafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/bubblesort_unsafe_false-valid-deref.i, 34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7.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 (34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7, sv-benchmarks/c/array-memsafety/bubblesort_unsafe_false-valid-deref.i).
Found 12 witnesses for program sv-benchmarks/c/array-memsafety/bubblesort_unsafe_false-valid-deref.i, 34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
5d3a002 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-09T20:53:11+01:00 |
b86831a |
2762b75 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-09T20:24:25+01:00 |
331b24d |
2e982fe |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
11 |
2018-12-08T22:10:46+01:00 |
39e381e |
b8a5693 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-08T04:35:26+01:00 |
c295304 |
c2c44dc |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
11 |
2018-12-06T09:02:20+01:00 |
2428013 |
93ed0ab |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-07T09:29:54+01:00 |
986a239 |
39e381e |
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-08T12:50:06 |
|
d9c61fe |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-09T20:37:24+01:00 |
33656d3 |
ac5e113 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-08T05:05:06+01:00 |
48813af |
3ac6a49 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-07T01:18:12+01:00 |
5adaee4 |
2dc4000 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-06T10:19:04+01:00 |
827d47e |
1abcc96 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
7 |
2018-12-06T09:18:13+01:00 |
a8725ed |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7, sv-benchmarks/c/array-memsafety/bubblesort_unsafe_false-valid-deref.i).
Found 10 witnesses for program sv-benchmarks/c/array-memsafety/bubblesort_unsafe_false-valid-deref.i, 34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
31f48bc |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
violation_witness |
Symbiotic |
1 |
2017-12-03T00:23 CET (sv-comp) |
|
de3d296 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
violation_witness |
ESBMC 4.6.0 kind |
4 |
2017-12-02T11:22:53.854523 |
|
f099ecc |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
violation_witness |
ESBMC 4.6.0 incr |
4 |
2017-12-01T23:19:56.035306 |
|
4f65308 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
violation_witness |
ESBMC 3.1 |
5 |
2017-12-01T09:15 CET (sv-comp) |
|
f4de474 |
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 |
|
58377e9 |
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-03T03:59Z |
|
0ecbd34 |
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:25 CET (sv-comp) |
|
27a878c |
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-03T04:21Z |
|
986a239 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
PredatorHP |
4 |
2017-12-01T22:14 CET (sv-comp) |
|
7aa2155 |
Inspect |
|
CHECK( init(main()), LTL(G valid-deref) ) |
violation_witness |
Map2Check |
2 |
2017-12-01T23:27 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7, sv-benchmarks/c/array-memsafety/bubblesort_unsafe_false-valid-deref.i).
Found 0 witnesses for program sv-benchmarks/c/array-memsafety/bubblesort_unsafe_false-valid-deref.i, 34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/34bf2416de06de2263e6327affac2c939c2f8f33716d2b1e86d3a9f0547479e7.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |