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 15 witnesses for program ../../../comp/sv-benchmarks/c/termination-memory-alloca/aviad_true-alloca_true-termination.c.i, da65a08be7a694e995d17e45362055fa5f60ddf40e08c5ba36204464b294ccf0
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/da65a08be7a694e995d17e45362055fa5f60ddf40e08c5ba36204464b294ccf0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
82bcec3 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T10:09:29+01:00 | ||
69888d3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-18T12:02:14+01:00 | 82bcec3 | |
2a1b525 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T07:33:08+01:00 | ||
0e00b00 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 5 | 2023-12-03T22:16:10+01:00 | ||
36661fd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2023-12-18T21:06:16+01:00 | ||
b111fc1 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.4.0 incr | 3 | 2023-12-01T10:46:13Z | ||
4ae0fe7 | 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 | 17 | 2023-12-02T18:03:08Z | ||
2f97590 | 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:25:50Z | ||
094a5d7 | 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-29T11:12:41Z | ||
32144bf | 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 | 17 | 2023-12-02T23:32:41Z | ||
13c6bd9 | 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) | 18 | 2023-12-01T01:29:52Z | ||
811b83a | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CBMC | 373 | 2023-12-17T17:58:14+01:00 | ||
d3f2f9a | 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 | 17 | 2023-11-29T05:57:36Z | ||
63659ca | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.4.0 | 3 | 2023-12-01T14:47:24Z | ||
7773b36 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 373 | 2023-12-17T17:50:35+01:00 |
Found 16 witnesses for program ../../../comp/sv-benchmarks/c/termination-memory-alloca/aviad_true-alloca_true-termination.c.i, da65a08be7a694e995d17e45362055fa5f60ddf40e08c5ba36204464b294ccf0
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/da65a08be7a694e995d17e45362055fa5f60ddf40e08c5ba36204464b294ccf0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c6c3f34 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T07:05:50+01:00 | ||
e7d8bc3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T14:19:21+01:00 | c6c3f34 | |
47f9adb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 5 | 2022-12-10T21:16:44+01:00 | ||
7eff79d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 5 | 2022-12-12T03:00:09+01:00 | ||
57aa124 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.0.0 incr | 3 | 2022-12-19T01:29:22Z | ||
00ffe8d | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2022-12-25T10:57:16Z | ||
756e3de | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2022-12-10T00:54:39+01:00 | ||
5b6d32f | 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 | 17 | 2022-12-14T13:04:52Z | ||
d0f6e78 | 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-11T10:10:11Z | ||
d1b4e99 | 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 | 17 | 2022-12-14T19:28:35Z | ||
4c67193 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CBMC | 373 | 2022-12-08T13:09:01+01:00 | ||
a793db3 | 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 | 16 | 2022-12-13T16:59:32Z | ||
93912e1 | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2022-12-25T09:52:19Z | ||
f747d56 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.0.0 | 3 | 2022-12-18T22:11:28Z | ||
5c64abd | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 373 | 2022-12-08T03:30:44+01:00 | ||
62c2659 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2022-12-08T17:55:03Z |
Found 3 witnesses for program ../../../comp/sv-benchmarks/c/termination-memory-alloca/aviad_true-alloca_true-termination.c.i, da65a08be7a694e995d17e45362055fa5f60ddf40e08c5ba36204464b294ccf0
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/da65a08be7a694e995d17e45362055fa5f60ddf40e08c5ba36204464b294ccf0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
14205be | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2021-12-08T06:16:11Z | ||
6741e1b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T17:47:59 | ||
7f06bf7 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 375 | 2021-12-06T10:38:11+01:00 |
Found 2 witnesses for program ../../../comp/sv-benchmarks/c/termination-memory-alloca/aviad_true-alloca_true-termination.c.i, da65a08be7a694e995d17e45362055fa5f60ddf40e08c5ba36204464b294ccf0
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/da65a08be7a694e995d17e45362055fa5f60ddf40e08c5ba36204464b294ccf0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3b12c1c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T19:17:38 | ||
347620e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T15:04:53 |
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/termination-memory-alloca/aviad_true-alloca_true-termination.c.i, da65a08be7a694e995d17e45362055fa5f60ddf40e08c5ba36204464b294ccf0
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/da65a08be7a694e995d17e45362055fa5f60ddf40e08c5ba36204464b294ccf0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/termination-memory-alloca/aviad_true-alloca_true-termination.c.i, da65a08be7a694e995d17e45362055fa5f60ddf40e08c5ba36204464b294ccf0
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/da65a08be7a694e995d17e45362055fa5f60ddf40e08c5ba36204464b294ccf0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 4 witnesses for program ../../../comp/sv-benchmarks/c/termination-memory-alloca/aviad_true-alloca_true-termination.c.i, da65a08be7a694e995d17e45362055fa5f60ddf40e08c5ba36204464b294ccf0
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/da65a08be7a694e995d17e45362055fa5f60ddf40e08c5ba36204464b294ccf0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
abe4422 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T00:51:49.810856 | ||
de8aa23 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T12:41:27.982028 | ||
aa49558 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 7 | 2017-12-01T21:12 CET (sv-comp) | ||
bf14cf0 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 398 | 2017-12-01T15:07 CET (sv-comp) |
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/termination-memory-alloca/aviad_true-alloca_true-termination.c.i, da65a08be7a694e995d17e45362055fa5f60ddf40e08c5ba36204464b294ccf0
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/da65a08be7a694e995d17e45362055fa5f60ddf40e08c5ba36204464b294ccf0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |