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_true-valid-memsafety_true-termination.i, aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c7cbffa | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2023-12-18T07:58:40+01:00 | ||
6896d67 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T19:19:08Z | ||
5771d23 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-30T08:33:29+01:00 | ||
c6efb39 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 8 | 2023-12-03T23:15:39+01:00 | ||
1277758 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 8 | 2023-12-19T14:00:54+01:00 | ||
042496b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 13 | 2023-12-18T02:00:40+01:00 | ||
1ad44b2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-05T09:05:38Z | ||
8afd827 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-04T12:49:14Z | ||
30de3e8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-01T21:13:53Z | ||
8f434ee | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.4.0 incr | 3 | 2023-12-01T13:02:36Z | ||
4d87616 | 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 | 9 | 2023-12-17T13:43:08+01:00 | ||
b784d14 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 8 | 2023-12-18T19:26:22+01:00 | ||
4c23eb6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.4.0 | 3 | 2023-12-01T14:31:26Z | ||
0c45988 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T16:47:04Z | ||
fa4564d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 3 | 2023-12-01T02:00:51Z | ||
18cbc0a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 7 | 2023-12-17T11:44:44+01:00 | ||
727100e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-05T09:48:28Z | ||
2069602 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-04T14:12:32Z | ||
698fdc9 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-01T19:51:26Z |
Found 15 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i, aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7da02be | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2022-12-09T07:04:06+01:00 | ||
35daadd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 8 | 2022-12-10T21:19:33+01:00 | ||
b3270aa | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 8 | 2022-12-11T19:41:37+01:00 | ||
2f2d84a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 8 | 2022-12-11T02:16:40+01:00 | ||
ba113ca | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 8 | 2022-12-09T17:40:51+01:00 | ||
c47f80f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 13 | 2022-12-09T03:01:42+01:00 | ||
a681a8a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2022-12-08T12:53:03Z | ||
2d0fa07 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.0.0 incr | 3 | 2022-12-18T22:28:00Z | ||
635204a | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2022-12-25T10:11:01Z | ||
e17b29b | 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 | 9 | 2022-12-08T11:06:46+01:00 | ||
74ded1a | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2022-12-25T09:56:18Z | ||
3c0dabc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.0.0 | 3 | 2022-12-18T23:13:53Z | ||
55dca0f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T16:04:25Z | ||
ec3c2c5 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 7 | 2022-12-08T13:33:54+01:00 | ||
4f2f68f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2022-12-08T14:51:07Z |
Found 10 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i, aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8c51bc0 | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2021-12-07T07:52:00+01:00 | ||
f9ed0ba | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 8 | 2021-12-05T15:21:16+01:00 | ||
f19bca7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 8 | 2021-12-09T12:02:50+01:00 | ||
fe2315c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 13 | 2021-12-07T01:57:28+01:00 | ||
d11a7b5 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2021-12-08T08:30:56Z | ||
dbe81b5 | 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 | 7 | 2021-12-06T03:37:08+01:00 | ||
e4065e8 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 8 | 2021-12-08T18:10:06+01:00 | ||
956df79 | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2021-12-08T03:33:23Z | ||
d686b65 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2021-12-07T14:29:33Z | ||
e4898af | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 7 | 2021-12-06T07:47:45+01:00 |
Found 5 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i, aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
873e310 | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2020-12-06T18:46:24+01:00 | ||
5427830 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 8 | 2020-12-05T15:54:29+01:00 | ||
f1b51ec | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 8 | 2020-12-08T00:40:25+01:00 | ||
c0eee24 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T21:38:18 | ||
eb0808e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-09T02:36:53 |
Found 2 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i, aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3a43cc0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 8 | 2019-11-30T00:10:22+01:00 | ||
add402b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 8 | 2019-12-01T03:46:32+01:00 |
Found 4 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i, aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9e9b286 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T14:01 CET (sv-comp) | ||
8c15e15 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 8 | 2018-12-06T13:18:43+01:00 | ||
dcb8780 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-05T18:29:26+01:00 | ||
a9b60f5 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T09:12 CET (sv-comp) |
Found 11 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i, aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
35f9c86 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-03T00:18 CET (sv-comp) | ||
a7ee104 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 3.1 | 7 | 2017-12-01T09:09 CET (sv-comp) | ||
f891e72 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T10:59:41.603388 | ||
2f2015c | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T23:58:39.284892 | ||
8c86436 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-12-01T08:24:16+01:00 | ||
c3e3f50 | 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:54 CET (sv-comp) | ||
b99477a | 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 | 2017-12-01T08:27 CET (sv-comp) | ||
061c3e5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T20:01:22.523406 | ||
5e87081 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T08:11:18.262408 | ||
25d56da | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 7 | 2017-12-01T16:39 CET (sv-comp) | ||
e63b03d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 11 | 2017-12-01T19:16 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i, aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/aa52a50db96d55b59d19995958546e1bde20387ce0b816cd9ff33848cc2087c5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |