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 27 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c, e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e9efd80 | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2023-12-18T10:20:15+01:00 | ||
041d1a9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T18:59:56Z | ||
245ae04 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-11-30T04:38:38+01:00 | ||
0601c30 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 3 | 2023-12-03T20:17:25+01:00 | ||
e880c56 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2023-12-18T23:55:14+01:00 | ||
a3179c8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2023-12-18T02:17:47+01:00 | ||
2c0b806 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-05T07:36:06Z | ||
0b8e412 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-04T12:29:14Z | ||
0bfae32 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-01T20:02:10Z | ||
27e3838 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.4.0 incr | 3 | 2023-12-01T10:26:21Z | ||
0169406 | 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 | 23 | 2023-12-02T14:36:50Z | ||
b314a80 | 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:26:07Z | ||
293221d | 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-29T06:38:59Z | ||
5b6e74b | 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 | 23 | 2023-12-02T22:41:52Z | ||
cef44c8 | 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-01T01:03:14Z | ||
d110896 | 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 | 2023-12-17T12:01:54+01:00 | ||
d258cd0 | 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 | 23 | 2023-11-29T04:56:18Z | ||
6e90faa | 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 | 4 | 2023-11-30T22:50:56+01:00 | ||
5cb7ada | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.4.0 | 3 | 2023-12-01T14:02:51Z | ||
a90921c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T20:07:14Z | ||
78d0a6f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2023-12-19T23:45:54 | ||
770c848 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 3 | 2023-12-01T02:05:01Z | ||
d5d2b3a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 5 | 2023-12-17T16:37:55+01:00 | ||
af94e10 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-05T10:00:38Z | ||
fc7ca16 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-04T14:31:11Z | ||
37e7e2b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-01T19:56:51Z | ||
7992dd6 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 4 | 2023-11-30T22:02:56+01:00 |
Found 21 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c, e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f7303e3 | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2022-12-09T06:22:04+01:00 | ||
3f40954 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2022-12-10T15:37:11+01:00 | ||
dd138cd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 3 | 2022-12-11T20:56:16+01:00 | ||
b9d0b47 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2022-12-09T23:31:39+01:00 | ||
23f243d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2022-12-09T03:13:03+01:00 | ||
a6388d3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2022-12-08T15:36:47Z | ||
6d47fb9 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.0.0 incr | 3 | 2022-12-18T16:32:52Z | ||
4d32285 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2022-12-25T11:25:45Z | ||
8119b86 | 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 | 23 | 2022-12-14T09:04:31Z | ||
1fa035b | 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:22:25Z | ||
3f278aa | 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 | 23 | 2022-12-15T01:44:15Z | ||
022d6aa | 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 | 2022-12-08T11:12:33+01:00 | ||
a50ed84 | 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 | 23 | 2022-12-13T20:49:03Z | ||
f549780 | 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 | 4 | 2022-12-08T02:14:20+01:00 | ||
8512e3f | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2022-12-25T10:37:19Z | ||
af5a4ae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.0.0 | 3 | 2022-12-19T01:34:28Z | ||
ffc54dd | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T14:32:58Z | ||
2cc5b3e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2022-12-11T17:34:40 | ||
23e3ef0 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 5 | 2022-12-08T11:28:54+01:00 | ||
1ff743f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2022-12-08T15:19:37Z | ||
40efcc8 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 4 | 2022-12-07T21:52:18+01:00 |
Found 17 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c, e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
75ec76d | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2021-12-07T10:00:15+01:00 | ||
4a43e04 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-05T15:01:58+01:00 | ||
f3c684e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 3 | 2021-12-08T20:32:45+01:00 | ||
02aced6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2021-12-07T03:34:06+01:00 | ||
3b9da73 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2021-12-08T09:12:41Z | ||
74688f5 | 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 | 23 | 2021-12-10T04:53:11Z | ||
fef9828 | 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 | 23 | 2021-12-10T10:47:02Z | ||
bf215e6 | 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 | 3 | 2021-12-06T08:07:32+01:00 | ||
5411388 | 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 | 23 | 2021-12-06T17:34:43Z | ||
bc77e47 | 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 | 4 | 2021-12-05T23:14:28+01:00 | ||
7d16372 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | SESL | 2 | 2021-12-06T11:27:24+01:00 | ||
2199b41 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2021-12-09T11:52:33+01:00 | ||
20aab09 | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2021-12-08T03:49:50Z | ||
1c31f60 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2021-12-07T17:21:01Z | ||
f912c58 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2021-12-09T06:08:18 | ||
b7dc191 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 3 | 2021-12-06T05:32:11+01:00 | ||
43b40df | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 4 | 2021-12-05T22:29:52+01:00 |
Found 6 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c, e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
79742d7 | Inspect | valid-memsafety | correctness_witness | DIVINE 4 | 2 | 2020-12-06T17:52:45+01:00 | ||
0a929e0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2020-12-07T23:58:33+01:00 | ||
f4637de | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0 | 3 | 2020-12-05T14:09:09+01:00 | ||
a005e64 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T15:38:15 | ||
d0a61a0 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T18:56:03 | ||
2701eaa | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2020-12-08T08:26:48 |
Found 3 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c, e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
db3c971 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 3 | 2019-11-30T23:43:03+01:00 | ||
3a4f7c6 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 3 | 2019-11-30T03:12:37+01:00 | ||
659a351 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-04T01:19 CET (comp) |
Found 5 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c, e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
efd7275 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T07:46 CET (sv-comp) | ||
eec99ac | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 3 | 2018-12-06T21:58:51+01:00 | ||
d05d2af | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T05:00:25+01:00 | ||
aa2b8ff | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T13:46 CET (sv-comp) | ||
407400f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T11:21 CET (sv-comp) |
Found 17 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c, e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3eb86d4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T23:31 CET (sv-comp) | ||
9c0e8b4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 3 | 2017-12-01T08:32:28+01:00 | ||
64d817a | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T10:42:49.465765 | ||
6a26bb7 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T23:53:22.113451 | ||
9ed580d | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.6.1-svn | 5 | 2017-12-01T09:14:46+01:00 | ||
b319768 | 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 | 3 | 2017-12-03T06:55Z | ||
36d9abc | 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:12 CET (sv-comp) | ||
f276e94 | 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-03T03:59Z | ||
014e0e9 | 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 | 4 | 2017-12-01T19:46 CET (sv-comp) | ||
6004a54 | 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 | 3 | 2017-12-01T08:27 CET (sv-comp) | ||
14ec756 | 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 | 3 | 2017-12-03T03:57Z | ||
aae3d60 | 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 | 4 | 2017-12-01T08:19 CET (sv-comp) | ||
38c42e8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T20:09:30.860063 | ||
ef73797 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T12:56:38.137781 | ||
c5b72d1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 4 | 2017-12-01T19:49 CET (sv-comp) | ||
cd13b13 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 3 | 2017-12-01T16:35 CET (sv-comp) | ||
1fe0475 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 4 | 2017-12-01T12:56 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c, e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/e0af411cbe463e50d2f658cbef67da9cc6723e28c1262169ce3b6aa7303dfb51.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |