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 17 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c, b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c64d642 | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2023-12-18T09:55:44+01:00 | ||
d20aa26 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T20:39:06Z | ||
38c2ebf | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-11-30T05:38:34+01:00 | ||
99ddafb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 3 | 2023-12-03T21:47:01+01:00 | ||
da966d2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2023-12-18T01:33:52+01:00 | ||
787ce7f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-05T10:08:25Z | ||
c7ae47c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-04T05:23:26Z | ||
e5a7e40 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-01T21:00:56Z | ||
12d7108 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.4.0 incr | 3 | 2023-12-01T15:42:48Z | ||
4bb3be7 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2023-12-18T18:13:26+01:00 | ||
af9211d | 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 | 121 | 2023-12-02T15:27:54Z | ||
3b7744b | 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:18Z | ||
709020e | 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 | 121 | 2023-12-02T20:54:54Z | ||
097a2d1 | 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) | 4 | 2023-11-30T22:42:46Z | ||
f2a1a17 | 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 | 14 | 2023-12-17T19:43:21+01:00 | ||
5abbeef | 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 | 121 | 2023-11-29T05:49:43Z | ||
04c0b02 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | 2LS | 5 | 2023-11-30T23:02:26+01:00 |
Found 13 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c, b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3ca4f1b | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2022-12-09T05:20:24+01:00 | ||
9494514 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2022-12-10T14:58:23+01:00 | ||
3473209 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 3 | 2022-12-12T02:09:44+01:00 | ||
b05b677 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2022-12-10T00:00:14+01:00 | ||
a0aea5f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2022-12-09T02:40:05+01:00 | ||
8e826ba | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2022-12-08T21:47:04Z | ||
04636d4 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.0.0 incr | 3 | 2022-12-18T19:07:59Z | ||
cdc8900 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2022-12-25T10:57:23Z | ||
b5d6c71 | 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 | 121 | 2022-12-14T08:40:35Z | ||
4b7e4c7 | 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 | 121 | 2022-12-14T22:54:04Z | ||
3d0a7a5 | 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 | 14 | 2022-12-08T03:25:19+01:00 | ||
4c7d379 | 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 | 121 | 2022-12-13T12:40:36Z | ||
30679d7 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | 2LS | 5 | 2022-12-08T01:19:56+01:00 |
Found 11 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c, b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3fb41db | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2021-12-07T09:28:21+01:00 | ||
bc66a83 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-05T17:55:47+01:00 | ||
4188bf6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 3 | 2021-12-08T20:12:04+01:00 | ||
b433888 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2021-12-07T02:22:02+01:00 | ||
49b8172 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2021-12-08T11:00:39Z | ||
a496a99 | 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 | 121 | 2021-12-10T02:24:00Z | ||
111a419 | 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 | 121 | 2021-12-10T08:22:01Z | ||
91c19b2 | 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 | 6 | 2021-12-06T02:22:13+01:00 | ||
fb5ff3f | 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 | 121 | 2021-12-06T18:12:06Z | ||
e03d2ef | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | 2LS | 5 | 2021-12-05T19:36:14+01:00 | ||
3a66b25 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2021-12-09T09:56:20+01:00 |
Found 3 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c, b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
de8bf11 | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2020-12-06T18:16:43+01:00 | ||
a7cc415 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2020-12-08T05:11:26+01:00 | ||
021c654 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0 | 3 | 2020-12-05T14:50:44+01:00 |
Found 2 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c, b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
cff3059 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 3 | 2019-11-30T12:50:25+01:00 | ||
653bcde | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 3 | 2019-12-01T05:55:52+01:00 |
Found 3 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c, b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
55151d7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T00:40 CET (sv-comp) | ||
eec067c | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 3 | 2018-12-07T05:44:58+01:00 | ||
d362f4d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-05T18:03:36+01:00 |
Found 8 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c, b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
56fd1cd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-03T00:29 CET (sv-comp) | ||
6594f07 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.6.1-svn | 5 | 2017-12-01T09:23:23+01:00 | ||
b9bfe1b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 3 | 2017-12-01T08:25:58+01:00 | ||
5cd3f2b | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T11:56:29.584798 | ||
3ebba9e | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T23:23:42.158760 | ||
55e3ff1 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Map2Check | 2 | 2017-12-01T23:54 CET (sv-comp) | ||
321d06f | 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 | 4 | 2017-12-01T08:30 CET (sv-comp) | ||
26e87ec | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | 2LS | 5 | 2017-12-01T08:20 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c, b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |