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 11 witnesses for program sv-benchmarks/c/termination-memory-alloca/easySum-alloca_true-termination.c.i, 4b46132106c9582d9b36bde1be1a9d4d3fc071854166953d5e72a8b88085e0ad
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/4b46132106c9582d9b36bde1be1a9d4d3fc071854166953d5e72a8b88085e0ad.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6a6cdbf | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T09:19:05+01:00 | ||
e77b56b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T21:42:10Z | ||
eba6465 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-18T12:02:39+01:00 | 6a6cdbf | |
0dd961c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T06:34:04+01:00 | ||
93fb6c7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 5 | 2023-12-03T18:33:58+01:00 | ||
64b8adf | 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 | 15 | 2023-12-02T17:39:41Z | ||
171aff4 | 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:24:57Z | ||
d7bb08c | 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-29T13:22:37Z | ||
eee3aaf | 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 | 15 | 2023-12-03T02:45:09Z | ||
84dae90 | 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) | 17 | 2023-12-01T01:42:27Z | ||
67a096a | 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 | 15 | 2023-11-28T22:29:52Z |
Found 9 witnesses for program sv-benchmarks/c/termination-memory-alloca/easySum-alloca_true-termination.c.i, 4b46132106c9582d9b36bde1be1a9d4d3fc071854166953d5e72a8b88085e0ad
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/4b46132106c9582d9b36bde1be1a9d4d3fc071854166953d5e72a8b88085e0ad.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ee903c7 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:43:00+01:00 | ||
0f79296 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T14:18:12+01:00 | ee903c7 | |
9ffcfe8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 5 | 2022-12-10T12:07:13+01:00 | ||
97873c0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 5 | 2022-12-12T02:46:34+01:00 | ||
a863624 | 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 | 14 | 2022-12-14T06:20:32Z | ||
4d3e0e3 | 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-11T09:25:18Z | ||
048c4a8 | 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 | 14 | 2022-12-14T19:45:57Z | ||
18fba24 | 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 | 14 | 2022-12-13T17:06:01Z | ||
e299516 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2022-12-08T17:22:09Z |
Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/easySum-alloca_true-termination.c.i, 4b46132106c9582d9b36bde1be1a9d4d3fc071854166953d5e72a8b88085e0ad
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/4b46132106c9582d9b36bde1be1a9d4d3fc071854166953d5e72a8b88085e0ad.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
fa9a882 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T18:50:47 |
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/easySum-alloca_true-termination.c.i, 4b46132106c9582d9b36bde1be1a9d4d3fc071854166953d5e72a8b88085e0ad
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/4b46132106c9582d9b36bde1be1a9d4d3fc071854166953d5e72a8b88085e0ad.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6b5959b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T15:50:07 | ||
3dfb02b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-09T00:38:01 |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/easySum-alloca_true-termination.c.i, 4b46132106c9582d9b36bde1be1a9d4d3fc071854166953d5e72a8b88085e0ad
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/4b46132106c9582d9b36bde1be1a9d4d3fc071854166953d5e72a8b88085e0ad.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/easySum-alloca_true-termination.c.i, 4b46132106c9582d9b36bde1be1a9d4d3fc071854166953d5e72a8b88085e0ad
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/4b46132106c9582d9b36bde1be1a9d4d3fc071854166953d5e72a8b88085e0ad.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
76b6fda | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T09:09 CET (sv-comp) |
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/easySum-alloca_true-termination.c.i, 4b46132106c9582d9b36bde1be1a9d4d3fc071854166953d5e72a8b88085e0ad
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/4b46132106c9582d9b36bde1be1a9d4d3fc071854166953d5e72a8b88085e0ad.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
da698f3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 6 | 2017-12-01T20:16 CET (sv-comp) | ||
315cbaa | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 27 | 2017-12-01T14:32 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/easySum-alloca_true-termination.c.i, 4b46132106c9582d9b36bde1be1a9d4d3fc071854166953d5e72a8b88085e0ad
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/4b46132106c9582d9b36bde1be1a9d4d3fc071854166953d5e72a8b88085e0ad.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |