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 12 witnesses for program sv-benchmarks/c/termination-memory-alloca/Avery-2006FLOPS-Tabel1_true-alloca_true-termination.c.i, d23b84347ad8f89b884566eade2030749c1dbcf7e12f4141b44403af4e899f5c
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/d23b84347ad8f89b884566eade2030749c1dbcf7e12f4141b44403af4e899f5c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
5ed371e | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T10:39:35+01:00 | ||
2846c9f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T19:41:06Z | ||
4683c59 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-18T12:04:17+01:00 | 5ed371e | |
cb6ad27 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T06:12:44+01:00 | ||
895e2ca | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 6 | 2023-12-03T22:12:31+01:00 | ||
fd6a205 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2023-12-18T16:35:22+01:00 | ||
7afcbcb | 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 | 26 | 2023-12-02T12:25:30Z | ||
f4db547 | 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:48Z | ||
b953fcc | 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:32:47Z | ||
860cbeb | 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 | 26 | 2023-12-02T21:26:16Z | ||
813b3cd | 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) | 30 | 2023-12-01T00:59:52Z | ||
fef7f75 | 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 | 26 | 2023-11-28T23:09:00Z |
Found 10 witnesses for program sv-benchmarks/c/termination-memory-alloca/Avery-2006FLOPS-Tabel1_true-alloca_true-termination.c.i, d23b84347ad8f89b884566eade2030749c1dbcf7e12f4141b44403af4e899f5c
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/d23b84347ad8f89b884566eade2030749c1dbcf7e12f4141b44403af4e899f5c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
21e1ae9 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T07:14:03+01:00 | ||
9fe3ba2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T12:56:08Z | ||
8cf6950 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T14:17:59+01:00 | 21e1ae9 | |
1876a50 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 6 | 2022-12-10T21:10:57+01:00 | ||
d6ce7bc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 6 | 2022-12-12T00:07:14+01:00 | ||
7484839 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2022-12-10T03:31:33+01:00 | ||
e124dd6 | 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 | 25 | 2022-12-14T09:05:23Z | ||
1f7c67e | 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:23:01Z | ||
c672a03 | 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 | 25 | 2022-12-14T22:14:04Z | ||
d62e457 | 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 | 25 | 2022-12-13T12:40:18Z |
Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/Avery-2006FLOPS-Tabel1_true-alloca_true-termination.c.i, d23b84347ad8f89b884566eade2030749c1dbcf7e12f4141b44403af4e899f5c
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/d23b84347ad8f89b884566eade2030749c1dbcf7e12f4141b44403af4e899f5c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
89b13e6 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T17:53:35 |
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/Avery-2006FLOPS-Tabel1_true-alloca_true-termination.c.i, d23b84347ad8f89b884566eade2030749c1dbcf7e12f4141b44403af4e899f5c
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/d23b84347ad8f89b884566eade2030749c1dbcf7e12f4141b44403af4e899f5c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
096440b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T21:24:01 | ||
fa0ed37 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T16:20:05 |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/Avery-2006FLOPS-Tabel1_true-alloca_true-termination.c.i, d23b84347ad8f89b884566eade2030749c1dbcf7e12f4141b44403af4e899f5c
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/d23b84347ad8f89b884566eade2030749c1dbcf7e12f4141b44403af4e899f5c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/Avery-2006FLOPS-Tabel1_true-alloca_true-termination.c.i, d23b84347ad8f89b884566eade2030749c1dbcf7e12f4141b44403af4e899f5c
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/d23b84347ad8f89b884566eade2030749c1dbcf7e12f4141b44403af4e899f5c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/Avery-2006FLOPS-Tabel1_true-alloca_true-termination.c.i, d23b84347ad8f89b884566eade2030749c1dbcf7e12f4141b44403af4e899f5c
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/d23b84347ad8f89b884566eade2030749c1dbcf7e12f4141b44403af4e899f5c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
61b8adb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 7 | 2017-12-01T21:09 CET (sv-comp) | ||
6a25aa0 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 43 | 2017-12-01T12:29 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/Avery-2006FLOPS-Tabel1_true-alloca_true-termination.c.i, d23b84347ad8f89b884566eade2030749c1dbcf7e12f4141b44403af4e899f5c
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/d23b84347ad8f89b884566eade2030749c1dbcf7e12f4141b44403af4e899f5c.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |