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 ../../../comp/sv-benchmarks/c/ldv-memsafety/memset3_true-valid-memsafety_true-termination.c, 0e16460170daade69818450e1395d982497f59eca845b3ed1031565545c18793
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/0e16460170daade69818450e1395d982497f59eca845b3ed1031565545c18793.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
90864b2 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T09:20:09+01:00 | ||
10e3a62 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T23:26:31Z | ||
b1b6975 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-18T12:05:14+01:00 | 90864b2 | |
0919bec | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-11-30T05:18:50+01:00 | ||
7a65180 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 3 | 2023-12-04T00:33:58+01:00 | ||
73a18af | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 4 | 2023-12-18T02:06:56+01:00 | ||
5b63816 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-05T12:51:55Z | ||
3c098ec | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-04T13:43:28Z | ||
b485a48 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-01T20:07:24Z | ||
51f5716 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.4.0 incr | 3 | 2023-12-01T16:07:12Z | ||
a02d6e7 | 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-02T07:17:36Z | ||
2fb59d0 | 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:06Z | ||
4efcf46 | 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-29T14:37:00Z | ||
ce64089 | 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-02T20:19:08Z | ||
164d381 | 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-01T02:08:11Z | ||
49fd7ab | 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-17T05:53:58+01:00 | ||
d8c029c | 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:10:34Z | ||
89fdc1b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0 | 3 | 2023-12-19T12:04:23+01:00 | ||
3b73a0a | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2023-12-18T18:25:47+01:00 | ||
660e598 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.4.0 | 3 | 2023-12-01T12:43:11Z | ||
17638de | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T22:01:47Z | ||
cd30019 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 3 | 2023-12-01T01:42:17Z | ||
98a6306 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 4 | 2023-12-17T14:30:32+01:00 | ||
8f86eea | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-05T11:15:35Z | ||
75cbffe | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-04T13:10:57Z | ||
3d1ccd6 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-01T19:51:14Z |
Found 20 witnesses for program ../../../comp/sv-benchmarks/c/ldv-memsafety/memset3_true-valid-memsafety_true-termination.c, 0e16460170daade69818450e1395d982497f59eca845b3ed1031565545c18793
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/0e16460170daade69818450e1395d982497f59eca845b3ed1031565545c18793.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1600f2f | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:30:44+01:00 | ||
aa42da7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-28T14:16:59+01:00 | 1600f2f | |
617c758 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2022-12-10T16:23:33+01:00 | ||
a2c568b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 3 | 2022-12-11T23:05:01+01:00 | ||
308013e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 3 | 2022-12-11T04:58:54+01:00 | ||
9238665 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2022-12-10T00:44:52+01:00 | ||
679014e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 4 | 2022-12-09T02:55:22+01:00 | ||
62a3734 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2022-12-08T14:37:38Z | ||
17f4189 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.0.0 incr | 3 | 2022-12-18T18:31:35Z | ||
fe6f5af | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2022-12-25T08:25:08Z | ||
58fcdcd | 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-14T03:57:21Z | ||
cba1964 | 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:29:17Z | ||
52a5bae | 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 | 2022-12-14T22:12:19Z | ||
0bcff48 | 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-08T07:51:29+01:00 | ||
ad6e4e8 | 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-13T16:03:57Z | ||
41b71aa | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2022-12-25T11:40:22Z | ||
997b937 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.0.0 | 3 | 2022-12-18T17:44:27Z | ||
56d5c3d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T10:13:10Z | ||
4414b0f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 4 | 2022-12-08T03:45:18+01:00 | ||
0984fe3 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 2 | 2022-12-08T20:16:45Z |
Found 13 witnesses for program ../../../comp/sv-benchmarks/c/ldv-memsafety/memset3_true-valid-memsafety_true-termination.c, 0e16460170daade69818450e1395d982497f59eca845b3ed1031565545c18793
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/0e16460170daade69818450e1395d982497f59eca845b3ed1031565545c18793.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
bc683a4 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T08:08:42+01:00 | ||
803e8ec | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-05T14:15:40+01:00 | ||
1c0b5bf | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2021-12-09T13:50:28+01:00 | ||
d2b9f5c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 4 | 2021-12-07T02:38:14+01:00 | ||
a07ba82 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2021-12-08T08:09:02Z | ||
c348e5f | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 3 | 2021-12-08T18:48:58+01:00 | ||
e6df335 | 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-10T00:03:24Z | ||
70f5af3 | 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 | 2021-12-10T11:10:45Z | ||
261c7e2 | 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-06T07:36:23+01:00 | ||
4bb3e1c | 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:44:45Z | ||
f75e6df | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2021-12-08T03:41:51Z | ||
cc1c0bb | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2021-12-07T10:12:53Z | ||
7e02502 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 4 | 2021-12-06T04:19:38+01:00 |
Found 5 witnesses for program ../../../comp/sv-benchmarks/c/ldv-memsafety/memset3_true-valid-memsafety_true-termination.c, 0e16460170daade69818450e1395d982497f59eca845b3ed1031565545c18793
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/0e16460170daade69818450e1395d982497f59eca845b3ed1031565545c18793.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
29f695d | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T18:13:25+01:00 | ||
c308fa8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 3 | 2020-12-05T15:39:01+01:00 | ||
7ec12b4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2020-12-08T01:36:00+01:00 | ||
c5461bb | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T18:59:13 | ||
9303a8c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-09T01:32:12 |
Found 2 witnesses for program ../../../comp/sv-benchmarks/c/ldv-memsafety/memset3_true-valid-memsafety_true-termination.c, 0e16460170daade69818450e1395d982497f59eca845b3ed1031565545c18793
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/0e16460170daade69818450e1395d982497f59eca845b3ed1031565545c18793.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
bd4bc25 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 3 | 2019-12-01T02:26:06+01:00 | ||
cce5a57 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 3 | 2019-11-30T12:39:23+01:00 |
Found 4 witnesses for program ../../../comp/sv-benchmarks/c/ldv-memsafety/memset3_true-valid-memsafety_true-termination.c, 0e16460170daade69818450e1395d982497f59eca845b3ed1031565545c18793
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/0e16460170daade69818450e1395d982497f59eca845b3ed1031565545c18793.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
fa6920e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T15:49 CET (sv-comp) | ||
1637651 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-05T09:25:43+01:00 | ||
92a8612 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 3 | 2018-12-07T03:32:00+01:00 | ||
52664df | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T04:17 CET (sv-comp) |
Found 14 witnesses for program ../../../comp/sv-benchmarks/c/ldv-memsafety/memset3_true-valid-memsafety_true-termination.c, 0e16460170daade69818450e1395d982497f59eca845b3ed1031565545c18793
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/0e16460170daade69818450e1395d982497f59eca845b3ed1031565545c18793.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
512b628 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-03T00:07 CET (sv-comp) | ||
1168792 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-01T09:45:39+01:00 | ||
7bc1cc7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 3 | 2017-12-01T08:28:35+01:00 | ||
3ff4467 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T11:10:55.671368 | ||
4d8e2a3 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T23:45:19.986384 | ||
6a51a78 | 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 | ||
ef50bf4 | 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 | 3 | 2017-12-01T23:50 CET (sv-comp) | ||
200a600 | 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 | 2017-12-03T04:28Z | ||
b1886b3 | 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 | 5 | 2017-12-01T08:24 CET (sv-comp) | ||
267e443 | 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-03T04:26Z | ||
1913018 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T20:57:37.567816 | ||
a335625 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T13:57:05.778374 | ||
ff7b520 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 5 | 2017-12-01T19:31 CET (sv-comp) | ||
dcdf0d2 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 4 | 2017-12-01T14:43 CET (sv-comp) |
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/ldv-memsafety/memset3_true-valid-memsafety_true-termination.c, 0e16460170daade69818450e1395d982497f59eca845b3ed1031565545c18793
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/0e16460170daade69818450e1395d982497f59eca845b3ed1031565545c18793.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |