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 26 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_true-valid-memsafety_true-termination.c, f0b671136c3b8e0a332730a51eabbaea09295c9938fd6e5af99480d4d2b7c8ed
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f0b671136c3b8e0a332730a51eabbaea09295c9938fd6e5af99480d4d2b7c8ed.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
bd24f89 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T07:58:38+01:00 | ||
cae955b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T19:31:48Z | ||
57bea7d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-18T12:04:32+01:00 | bd24f89 | |
1c848d2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-11-30T05:16:09+01:00 | ||
29af283 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 3 | 2023-12-03T20:56:31+01:00 | ||
c4a9d01 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 3 | 2023-12-19T13:07:55+01:00 | ||
5b683be | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2023-12-19T00:14:00+01:00 | ||
70b8071 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2023-12-18T01:44:38+01:00 | ||
d27cd4d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-05T11:49:35Z | ||
7b26f0b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-04T08:59:52Z | ||
ea9e126 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-01T20:59:42Z | ||
9282dc6 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.4.0 incr | 3 | 2023-12-01T14:28:36Z | ||
acdf188 | 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 | 5 | 2023-12-02T13:02:03Z | ||
244be06 | 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:27Z | ||
a65b08d | 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-29T09:03:18Z | ||
d4ea4a5 | 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 | 5 | 2023-12-03T02:26:46Z | ||
eaccdb0 | 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-12-01T00:56:27Z | ||
f498d9a | 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 | 2023-12-17T08:27:12+01:00 | ||
f68072e | 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 | 5 | 2023-11-28T23:02:32Z | ||
b34ea92 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.4.0 | 3 | 2023-12-01T13:21:28Z | ||
4ee7f1e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T16:44:21Z | ||
961fa20 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 3 | 2023-12-01T01:24:23Z | ||
ed526a8 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 3 | 2023-12-17T09:13:42+01:00 | ||
1ede1b0 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-05T11:16:07Z | ||
76c405c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-04T14:27:40Z | ||
de90b10 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-01T20:36:48Z |
Found 20 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_true-valid-memsafety_true-termination.c, f0b671136c3b8e0a332730a51eabbaea09295c9938fd6e5af99480d4d2b7c8ed
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f0b671136c3b8e0a332730a51eabbaea09295c9938fd6e5af99480d4d2b7c8ed.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e3c7e92 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:52:16+01:00 | ||
d5616f8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-28T14:21:14+01:00 | e3c7e92 | |
7a1666c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2022-12-10T21:20:31+01:00 | ||
fac1bb4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 3 | 2022-12-12T00:38:50+01:00 | ||
e38d4d1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 3 | 2022-12-11T05:47:09+01:00 | ||
5624d80 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2022-12-09T02:41:51+01:00 | ||
2fa11a1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2022-12-08T16:18:27Z | ||
a117c63 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.0.0 incr | 3 | 2022-12-18T19:14:16Z | ||
f83f33d | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2022-12-25T10:29:26Z | ||
a655efd | 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 | 4 | 2022-12-14T14:09:28Z | ||
a640082 | 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:16Z | ||
156342b | 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 | 4 | 2022-12-15T00:38:23Z | ||
8fb7f67 | 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 | 2022-12-08T08:41:12+01:00 | ||
5bf00f7 | 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 | 4 | 2022-12-13T18:27:07Z | ||
3a1df5d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2022-12-10T00:41:32+01:00 | ||
511b20b | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2022-12-25T09:57:49Z | ||
9db7d41 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.0.0 | 3 | 2022-12-18T18:22:18Z | ||
ed1815e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T12:56:19Z | ||
446864b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 3 | 2022-12-08T12:18:10+01:00 | ||
29e67ac | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 2 | 2022-12-08T18:55:03Z |
Found 13 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_true-valid-memsafety_true-termination.c, f0b671136c3b8e0a332730a51eabbaea09295c9938fd6e5af99480d4d2b7c8ed
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f0b671136c3b8e0a332730a51eabbaea09295c9938fd6e5af99480d4d2b7c8ed.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
27f3931 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T09:33:48+01:00 | ||
1fa4383 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-05T14:27:08+01:00 | ||
475d848 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2021-12-09T10:31:48+01:00 | ||
294c1c5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2021-12-07T02:01:59+01:00 | ||
aa1b6c7 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2021-12-08T09:24:55Z | ||
138c8ef | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 3 | 2021-12-08T20:27:26+01:00 | ||
cbfcdb8 | 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 | 4 | 2021-12-10T05:27:38Z | ||
184ffdb | 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 | 4 | 2021-12-10T09:23:03Z | ||
9d02a7f | 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 | 2021-12-06T09:05:52+01:00 | ||
ffe9769 | 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 | 4 | 2021-12-06T22:13:07Z | ||
b1358f6 | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2021-12-08T03:42:09Z | ||
17c4155 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2021-12-07T14:59:12Z | ||
ad4898b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 3 | 2021-12-06T04:10:46+01:00 |
Found 5 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_true-valid-memsafety_true-termination.c, f0b671136c3b8e0a332730a51eabbaea09295c9938fd6e5af99480d4d2b7c8ed
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f0b671136c3b8e0a332730a51eabbaea09295c9938fd6e5af99480d4d2b7c8ed.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a9b3df9 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T12:06:41+01:00 | ||
72ce799 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0 | 3 | 2020-12-05T15:27:56+01:00 | ||
1834d33 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2020-12-08T03:54:41+01:00 | ||
efe3969 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T21:33:14 | ||
e64c2a5 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T21:56:46 |
Found 2 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_true-valid-memsafety_true-termination.c, f0b671136c3b8e0a332730a51eabbaea09295c9938fd6e5af99480d4d2b7c8ed
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f0b671136c3b8e0a332730a51eabbaea09295c9938fd6e5af99480d4d2b7c8ed.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3736f96 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 3 | 2019-11-29T22:55:04+01:00 | ||
05c83fe | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 3 | 2019-12-01T12:37:05+01:00 |
Found 4 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_true-valid-memsafety_true-termination.c, f0b671136c3b8e0a332730a51eabbaea09295c9938fd6e5af99480d4d2b7c8ed
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f0b671136c3b8e0a332730a51eabbaea09295c9938fd6e5af99480d4d2b7c8ed.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c08d8e0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T16:44 CET (sv-comp) | ||
1761edb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 3 | 2018-12-08T00:31:33+01:00 | ||
e7025f2 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T06:30:19+01:00 | ||
a00e146 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-07T22:40 CET (sv-comp) |
Found 15 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_true-valid-memsafety_true-termination.c, f0b671136c3b8e0a332730a51eabbaea09295c9938fd6e5af99480d4d2b7c8ed
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f0b671136c3b8e0a332730a51eabbaea09295c9938fd6e5af99480d4d2b7c8ed.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e66f5f4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T23:17 CET (sv-comp) | ||
b270214 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-01T09:41:59+01:00 | ||
98e987b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 3 | 2017-12-01T08:34:13+01:00 | ||
23346fb | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T11:26:49.170141 | ||
81134e3 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T23:24:42.459354 | ||
4a3957c | 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 | 4 | 2017-12-03T06:53Z | ||
3c6805d | 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:47 CET (sv-comp) | ||
b2af641 | 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 | 3 | 2017-12-03T04:27Z | ||
ee4320b | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Forester | 5 | 2017-12-01T19:27 CET (sv-comp) | ||
6677882 | 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:21 CET (sv-comp) | ||
b45ded0 | 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 | 4 | 2017-12-03T03:54Z | ||
71bc1bc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T20:49:55.398107 | ||
d450e03 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T09:56:03.969179 | ||
f1fe0e5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 5 | 2017-12-01T21:30 CET (sv-comp) | ||
d97cdf6 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 3 | 2017-12-01T18:43 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_true-valid-memsafety_true-termination.c, f0b671136c3b8e0a332730a51eabbaea09295c9938fd6e5af99480d4d2b7c8ed
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f0b671136c3b8e0a332730a51eabbaea09295c9938fd6e5af99480d4d2b7c8ed.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |