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 19 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i, c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a5a8039 | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2023-12-18T09:50:47+01:00 | ||
4ab7532 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T23:25:26Z | ||
63c213d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T05:15:03+01:00 | ||
bccda4b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 6 | 2023-12-03T23:04:29+01:00 | ||
56ef23b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 9 | 2023-12-18T02:13:21+01:00 | ||
730265b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-05T10:24:07Z | ||
8522521 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-04T14:28:20Z | ||
9436f80 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-01T20:50:40Z | ||
65cb3e7 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.4.0 incr | 3 | 2023-12-01T03:24:35Z | ||
37c9e65 | 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 | 8 | 2023-12-17T12:41:37+01:00 | ||
e567e36 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0 | 6 | 2023-12-19T10:48:44+01:00 | ||
3a8f1c6 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2023-12-19T01:52:36+01:00 | ||
8055fae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.4.0 | 3 | 2023-12-01T10:11:08Z | ||
ca74d93 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T20:54:29Z | ||
c47910d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 3 | 2023-11-30T22:33:36Z | ||
196567f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 6 | 2023-12-17T08:55:21+01:00 | ||
ba5f98d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-05T12:34:23Z | ||
411311a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-04T09:09:50Z | ||
3df6c78 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-01T19:45:36Z |
Found 16 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i, c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7dcb6b8 | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2022-12-09T05:09:10+01:00 | ||
8492843 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T11:52:53Z | ||
a5c8368 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 6 | 2022-12-10T17:52:02+01:00 | ||
01019e6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 6 | 2022-12-12T02:14:37+01:00 | ||
e489937 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 6 | 2022-12-11T03:54:07+01:00 | ||
fbb87e6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2022-12-10T01:25:08+01:00 | ||
0c3ba03 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 9 | 2022-12-09T03:25:35+01:00 | ||
1135d7b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2022-12-08T21:12:32Z | ||
f551f1e | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.0.0 incr | 3 | 2022-12-18T21:39:24Z | ||
75e57af | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2022-12-25T09:36:15Z | ||
f97b1a8 | 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 | 8 | 2022-12-08T04:31:18+01:00 | ||
5cff0e7 | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2022-12-25T09:48:39Z | ||
d9871c1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.0.0 | 3 | 2022-12-19T02:40:13Z | ||
f8b3aa8 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T14:33:39Z | ||
46c71d2 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 6 | 2022-12-08T07:25:59+01:00 | ||
445b609 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2022-12-08T16:25:42Z |
Found 11 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i, c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2da0e94 | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2021-12-07T09:12:55+01:00 | ||
e4e7075 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2021-12-07T15:33:35Z | ||
672fc96 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 6 | 2021-12-05T17:23:03+01:00 | ||
2f50c25 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 9 | 2021-12-07T02:03:40+01:00 | ||
554b6d7 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2021-12-08T06:24:03Z | ||
a50bbc7 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 6 | 2021-12-08T19:34:11+01:00 | ||
80b26dc | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 6 | 2021-12-09T11:50:17+01:00 | ||
895893c | 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-06T10:58:42+01:00 | ||
d06c781 | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2021-12-08T03:38:52Z | ||
15aa312 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2021-12-07T12:06:21Z | ||
02ed330 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 6 | 2021-12-06T10:27:09+01:00 |
Found 7 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i, c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d0ab158 | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2020-12-06T18:45:55+01:00 | ||
fff151c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T21:05:06 | ||
40f6068 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 2 | 2020-12-09T02:25:57 | ||
7649277 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0 | 6 | 2020-12-05T12:58:46+01:00 | ||
e2ea0f6 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 6 | 2020-12-08T05:19:49+01:00 | ||
6a6555b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T23:07:08 | ||
6ec8c93 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T23:47:02 |
Found 2 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i, c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6b4f8a5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 6 | 2019-11-29T22:57:01+01:00 | ||
b26fc16 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 6 | 2019-12-01T04:40:19+01:00 |
Found 4 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i, c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1c0b37c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T16:53 CET (sv-comp) | ||
9d85aea | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 6 | 2018-12-08T00:52:03+01:00 | ||
d7baaa1 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-05T20:20:02+01:00 | ||
56fe724 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T04:42 CET (sv-comp) |
Found 11 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i, c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b6fe4fc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-03T00:05 CET (sv-comp) | ||
10f370c | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 3.1 | 7 | 2017-12-01T09:16 CET (sv-comp) | ||
a4c28c9 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T10:38:57.100653 | ||
ae2f75c | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T23:05:36.102980 | ||
2e88be7 | 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 | 4 | 2017-12-01T23:26 CET (sv-comp) | ||
9875812 | 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 | 13 | 2017-12-01T08:30 CET (sv-comp) | ||
dd7d909 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-01T08:29:31+01:00 | ||
78dfd27 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T19:42:33.483531 | ||
eface54 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T09:48:49.425197 | ||
30bd90e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 6 | 2017-12-01T21:27 CET (sv-comp) | ||
41d86ce | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 8 | 2017-12-01T13:28 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i, c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/c8e6193201f070e4e8fd99485640ffa2e10139023e39442c320d13bfe62360e5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |