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).
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test22_4_false-valid-memtrack_true-termination.i, f00f42c448f9e91b38c5651709147a617f4427b1e91516050b948f043f0c084d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f00f42c448f9e91b38c5651709147a617f4427b1e91516050b948f043f0c084d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test22_4_false-valid-memtrack_true-termination.i, f00f42c448f9e91b38c5651709147a617f4427b1e91516050b948f043f0c084d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f00f42c448f9e91b38c5651709147a617f4427b1e91516050b948f043f0c084d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test22_4_false-valid-memtrack_true-termination.i, f00f42c448f9e91b38c5651709147a617f4427b1e91516050b948f043f0c084d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f00f42c448f9e91b38c5651709147a617f4427b1e91516050b948f043f0c084d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test22_4_false-valid-memtrack_true-termination.i, f00f42c448f9e91b38c5651709147a617f4427b1e91516050b948f043f0c084d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f00f42c448f9e91b38c5651709147a617f4427b1e91516050b948f043f0c084d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test22_4_false-valid-memtrack_true-termination.i, f00f42c448f9e91b38c5651709147a617f4427b1e91516050b948f043f0c084d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f00f42c448f9e91b38c5651709147a617f4427b1e91516050b948f043f0c084d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test22_4_false-valid-memtrack_true-termination.i, f00f42c448f9e91b38c5651709147a617f4427b1e91516050b948f043f0c084d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f00f42c448f9e91b38c5651709147a617f4427b1e91516050b948f043f0c084d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ea5b474 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T13:16 CET (sv-comp) | ||
a4922cb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 19 | 2018-12-06T13:39:53+01:00 | ||
51abcff | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 18 | 2018-12-08T09:06:56+01:00 | a4922cb | |
7edafbb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 18 | 2018-12-06T09:47:59+01:00 | 64fcab5 | |
4c9a04d | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-07T09:21:28+01:00 | f3a0b7e | |
e61192f | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-06T09:17:20+01:00 | a6776bb | |
e8dad42 | 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-08T08:58:46 | ||
23b90af | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-08T23:44:04+01:00 | ea5b474 | |
0077332 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 18 | 2018-12-08T22:09:53+01:00 | e8dad42 | |
bf2ad73 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-07T01:19:51+01:00 | 5677393 | |
64fcab5 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 19 | 2018-12-05T18:44:11+01:00 | ||
ffa3f95 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-08T05:02:01+01:00 | d993835 | |
2ba0872 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-06T10:15:03+01:00 | 47b0992 | |
806e9a5 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T00:08 CET (sv-comp) |
Found 12 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test22_4_false-valid-memtrack_true-termination.i, f00f42c448f9e91b38c5651709147a617f4427b1e91516050b948f043f0c084d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f00f42c448f9e91b38c5651709147a617f4427b1e91516050b948f043f0c084d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
30e0400 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-02T23:28 CET (sv-comp) | ||
f3a0b7e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | PredatorHP | 6 | 2017-12-01T22:06 CET (sv-comp) | ||
bae8a59 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Map2Check | 2 | 2017-12-01T23:29 CET (sv-comp) | ||
1744a13 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 10 | 2017-12-02T11:58:24.761569 | ||
b1d5810 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 10 | 2017-12-01T23:38:07.324155 | ||
a3d3e80 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 3.1 | 10 | 2017-12-01T09:39 CET (sv-comp) | ||
5472783 | 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 | 22 | 2017-12-01T08:21 CET (sv-comp) | ||
0c6c613 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-01T08:25:51+01:00 | ||
8dc5ae2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T20:47:53.907483 | ||
356e581 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T10:25:33.408362 | ||
8fe3a6c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 18 | 2017-12-01T16:32 CET (sv-comp) | ||
02fae1e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 21 | 2017-12-01T16:44 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test22_4_false-valid-memtrack_true-termination.i, f00f42c448f9e91b38c5651709147a617f4427b1e91516050b948f043f0c084d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f00f42c448f9e91b38c5651709147a617f4427b1e91516050b948f043f0c084d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |