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 24 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i, 337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e1fc3c3 | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2023-12-18T09:51:57+01:00 | ||
ff4b435 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T23:12:46Z | ||
6d1e2d7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T04:54:54+01:00 | ||
dc552d1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 5 | 2023-12-03T18:07:47+01:00 | ||
14c699e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2023-12-19T02:09:09+01:00 | ||
413f7a3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 6 | 2023-12-18T02:16:03+01:00 | ||
8364e77 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-05T10:18:40Z | ||
00543c9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-04T13:24:50Z | ||
012a69b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-01T20:25:04Z | ||
802fc33 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.4.0 incr | 3 | 2023-12-01T12:50:49Z | ||
cecd785 | 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 | 11 | 2023-12-02T12:08:16Z | ||
0a5a87e | 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:39Z | ||
87ffebe | 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-29T12:45:56Z | ||
a74e31c | 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 | 11 | 2023-12-02T22:13:06Z | ||
5a44f33 | 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) | 7 | 2023-12-01T01:43:53Z | ||
8ea0380 | 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 | 19 | 2023-12-17T13:53:45+01:00 | ||
558ebef | 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 | 11 | 2023-11-28T23:41:56Z | ||
2ab83e8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.4.0 | 3 | 2023-12-01T14:09:59Z | ||
1cdb03a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T21:57:15Z | ||
49813f8 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2023-12-19T22:56:06 | ||
c3670b8 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 19 | 2023-12-17T10:19:16+01:00 | ||
bda049c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-05T08:08:20Z | ||
3d88eff | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-04T13:06:16Z | ||
95ad47d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-01T20:44:41Z |
Found 19 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i, 337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c792124 | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2022-12-09T05:10:42+01:00 | ||
85b1004 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 5 | 2022-12-10T19:40:30+01:00 | ||
fb6c6d8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 5 | 2022-12-12T02:49:24+01:00 | ||
73e6482 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2022-12-10T00:09:03+01:00 | ||
073405a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 6 | 2022-12-09T02:58:42+01:00 | ||
0b91272 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2022-12-08T19:18:53Z | ||
15823df | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.0.0 incr | 3 | 2022-12-18T23:24:25Z | ||
ec08a96 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2022-12-25T11:57:43Z | ||
70743b8 | 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 | 11 | 2022-12-14T14:06:24Z | ||
3a65c8d | 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-11T11:17:55Z | ||
2c53e73 | 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 | 11 | 2022-12-14T20:23:03Z | ||
b582ba1 | 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 | 19 | 2022-12-08T06:12:39+01:00 | ||
cfd07ef | 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 | 11 | 2022-12-13T17:11:29Z | ||
9f0f103 | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2022-12-25T08:24:59Z | ||
e948a72 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.0.0 | 3 | 2022-12-18T23:24:26Z | ||
ca1779a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T10:52:03Z | ||
aa2d1c1 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2022-12-11T14:08:45 | ||
ba811ca | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 19 | 2022-12-08T05:30:29+01:00 | ||
840cf35 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2022-12-08T19:42:41Z |
Found 4 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i, 337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b9135a8 | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2021-12-08T05:04:52Z | ||
219fc55 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2021-12-07T14:15:14Z | ||
51f5cfe | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2021-12-09T06:34:49 | ||
875b3ad | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 18 | 2021-12-06T10:50:19+01:00 |
Found 3 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i, 337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3231057 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T23:55:45 | ||
59dccb9 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T20:07:16 | ||
a32930b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2020-12-08T08:28:12 |
Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i, 337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
cf50b80 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:41 CET (comp) |
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i, 337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ea056c1 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T16:00 CET (sv-comp) | ||
9be139b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-06T23:54 CET (sv-comp) |
Found 5 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i, 337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a10eee7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T21:08:29.534920 | ||
8835c7f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T09:16:27.560996 | ||
87439fa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 5 | 2017-12-01T21:07 CET (sv-comp) | ||
43f6928 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 19 | 2017-12-01T16:09 CET (sv-comp) | ||
736e5d2 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 19 | 2017-12-01T12:07 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/java_Continue1-alloca_true-termination.c.i, 337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/337340cdf38da99928295b0c576766fb8f09c8634f9763511165b0f7240edd89.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |