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-15/count_up_and_down_alloca_true-termination.c.i, 00bfc508b8ea24f88f85b042e795fbae14e8287990a04ebdf542583ad129e19a
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/00bfc508b8ea24f88f85b042e795fbae14e8287990a04ebdf542583ad129e19a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2cec0d8 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T10:52:48+01:00 | ||
a901883 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-30T00:05:07Z | ||
708795e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-18T12:04:22+01:00 | 2cec0d8 | |
274edfa | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-30T04:52:48+01:00 | ||
ddc3050 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 7 | 2023-12-03T21:13:10+01:00 | ||
0ed6744 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2023-12-18T17:56:51+01:00 | ||
ae03121 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 10 | 2023-12-18T02:19:51+01:00 | ||
7bc4963 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0 | 7 | 2023-12-19T13:32:31+01:00 | ||
08f53c3 | 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 | 12 | 2023-12-02T18:21:03Z | ||
9ae8194 | 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-29T10:43:50Z | ||
409c1a0 | 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 | 12 | 2023-11-29T05:35:56Z |
Found 15 witnesses for program sv-benchmarks/c/termination-15/count_up_and_down_alloca_true-termination.c.i, 00bfc508b8ea24f88f85b042e795fbae14e8287990a04ebdf542583ad129e19a
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/00bfc508b8ea24f88f85b042e795fbae14e8287990a04ebdf542583ad129e19a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ae4cfbd | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:33:35+01:00 | ||
9ba0b58 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T15:43:17+01:00 | e5ce973 | |
700394c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T02:25:06+01:00 | 568c07d | |
bf7c8f7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T17:25:14Z | ||
62d6394 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T14:19:37+01:00 | ae4cfbd | |
51d5ef0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 7 | 2022-12-10T21:33:06+01:00 | ||
033c200 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 7 | 2022-12-12T02:51:20+01:00 | ||
dd3ab1f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 7 | 2022-12-11T05:04:01+01:00 | ||
d062b07 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2022-12-09T17:16:17+01:00 | ||
413122a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 10 | 2022-12-09T02:36:21+01:00 | ||
e5ce973 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 4 | 2022-12-19T00:38:52Z | ||
568c07d | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2022-12-25T10:37:00Z | ||
14fd3ab | 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 | 12 | 2022-12-14T10:24:02Z | ||
1974707 | 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:53:39Z | ||
fc7ab90 | 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 | 12 | 2022-12-13T16:56:38Z |
Found 0 witnesses for program sv-benchmarks/c/termination-15/count_up_and_down_alloca_true-termination.c.i, 00bfc508b8ea24f88f85b042e795fbae14e8287990a04ebdf542583ad129e19a
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/00bfc508b8ea24f88f85b042e795fbae14e8287990a04ebdf542583ad129e19a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-15/count_up_and_down_alloca_true-termination.c.i, 00bfc508b8ea24f88f85b042e795fbae14e8287990a04ebdf542583ad129e19a
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/00bfc508b8ea24f88f85b042e795fbae14e8287990a04ebdf542583ad129e19a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-15/count_up_and_down_alloca_true-termination.c.i, 00bfc508b8ea24f88f85b042e795fbae14e8287990a04ebdf542583ad129e19a
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/00bfc508b8ea24f88f85b042e795fbae14e8287990a04ebdf542583ad129e19a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-15/count_up_and_down_alloca_true-termination.c.i, 00bfc508b8ea24f88f85b042e795fbae14e8287990a04ebdf542583ad129e19a
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/00bfc508b8ea24f88f85b042e795fbae14e8287990a04ebdf542583ad129e19a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 1 witnesses for program sv-benchmarks/c/termination-15/count_up_and_down_alloca_true-termination.c.i, 00bfc508b8ea24f88f85b042e795fbae14e8287990a04ebdf542583ad129e19a
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/00bfc508b8ea24f88f85b042e795fbae14e8287990a04ebdf542583ad129e19a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
5e0bb67 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 8 | 2017-12-01T18:29 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-15/count_up_and_down_alloca_true-termination.c.i, 00bfc508b8ea24f88f85b042e795fbae14e8287990a04ebdf542583ad129e19a
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/00bfc508b8ea24f88f85b042e795fbae14e8287990a04ebdf542583ad129e19a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |