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/memsetNonZero3_true-valid-memsafety_true-termination.c, 51393d639f010eae1b63625f7a13f75512f9f6892d9718dd03fa54720c8c54a0
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/51393d639f010eae1b63625f7a13f75512f9f6892d9718dd03fa54720c8c54a0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
031319b | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T09:55:28+01:00 | ||
266f098 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T19:24:46Z | ||
60733d1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-18T12:07:07+01:00 | 031319b | |
d3604d6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-11-30T06:59:38+01:00 | ||
9e96c81 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 3 | 2023-12-04T00:40:58+01:00 | ||
c1db707 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2023-12-18T20:15:55+01:00 | ||
f442ae9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 4 | 2023-12-18T02:18:57+01:00 | ||
70a781d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-05T10:28:06Z | ||
6cb8ac6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-04T08:52:14Z | ||
c8175e4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-01T19:58:11Z | ||
afcc608 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.4.0 incr | 3 | 2023-12-01T10:36:51Z | ||
17af6ea | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0 | 3 | 2023-12-19T13:11:08+01:00 | ||
1993f57 | 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-02T12:15:03Z | ||
605b89a | 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:43Z | ||
758b096 | 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-29T10:33:38Z | ||
0f1a215 | 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-03T00:18:51Z | ||
ec698ff | 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:53:49Z | ||
34e880c | 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-17T12:27:09+01:00 | ||
35215d1 | 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-29T03:29:02Z | ||
0f817f6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.4.0 | 3 | 2023-12-01T03:23:10Z | ||
2216cf7 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2023-12-17T03:52:50Z | ||
c0aae92 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T21:00:58Z | ||
a874809 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 3 | 2023-11-30T22:37:52Z | ||
987e39f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 4 | 2023-12-17T14:28:00+01:00 | ||
674b9ee | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-05T07:12:59Z | ||
2b0e64e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-04T08:47:13Z | ||
bea6457 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-01T20:40:55Z |
Found 20 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero3_true-valid-memsafety_true-termination.c, 51393d639f010eae1b63625f7a13f75512f9f6892d9718dd03fa54720c8c54a0
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/51393d639f010eae1b63625f7a13f75512f9f6892d9718dd03fa54720c8c54a0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
855c518 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T07:11:36+01:00 | ||
929156e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-28T14:11:01+01:00 | 855c518 | |
d250fe6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2022-12-10T17:29:31+01:00 | ||
3dcc7ba | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 3 | 2022-12-11T21:11:07+01:00 | ||
668b528 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 4 | 2022-12-09T03:05:25+01:00 | ||
69d4440 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2022-12-08T21:19:47Z | ||
768893d | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.0.0 incr | 3 | 2022-12-19T00:58:45Z | ||
f3b0e9c | 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-14T04:04:47Z | ||
263b106 | 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:30:37Z | ||
321bf41 | 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:59:50Z | ||
f25e872 | 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-08T13:04:28+01:00 | ||
5d20f33 | 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-13T10:24:58Z | ||
c08ff2d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0 | 3 | 2022-12-11T05:17:37+01:00 | ||
f34e07c | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2022-12-10T02:00:32+01:00 | ||
a27e34f | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2022-12-25T08:50:01Z | ||
f546fdf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.0.0 | 3 | 2022-12-18T17:14:28Z | ||
5131b9a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2022-12-25T08:50:01Z | ||
be8137a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T13:13:25Z | ||
8ffba24 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 4 | 2022-12-08T10:42:49+01:00 | ||
4a1dd29 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2022-12-08T14:41:39Z |
Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero3_true-valid-memsafety_true-termination.c, 51393d639f010eae1b63625f7a13f75512f9f6892d9718dd03fa54720c8c54a0
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/51393d639f010eae1b63625f7a13f75512f9f6892d9718dd03fa54720c8c54a0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
0b39b60 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T07:55:57+01:00 | ||
04d7e77 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-05T14:24:47+01:00 | ||
4735d58 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 3 | 2021-12-08T19:59:52+01:00 | ||
354234f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2021-12-09T14:30:01+01:00 | ||
af2d383 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 4 | 2021-12-07T02:11:06+01:00 | ||
453f8fb | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2021-12-08T08:02:50Z | ||
ec744cb | 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-10T06:52:42Z | ||
107b6df | 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-10T13:07:19Z | ||
06abe64 | 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:28:46+01:00 | ||
412cee2 | 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-06T17:01:45Z | ||
f0223a9 | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2021-12-08T07:11:40Z | ||
a0bce0f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T17:02:15 | ||
1131269 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2021-12-07T12:24:25Z | ||
acf8cb7 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 4 | 2021-12-06T09:35:58+01:00 |
Found 5 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero3_true-valid-memsafety_true-termination.c, 51393d639f010eae1b63625f7a13f75512f9f6892d9718dd03fa54720c8c54a0
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/51393d639f010eae1b63625f7a13f75512f9f6892d9718dd03fa54720c8c54a0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
701c66c | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T18:43:56+01:00 | ||
895ab06 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0 | 3 | 2020-12-05T12:57:14+01:00 | ||
bc5592d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2020-12-07T22:55:36+01:00 | ||
b928e20 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T19:48:56 | ||
7c2c003 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-09T01:55:47 |
Found 2 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero3_true-valid-memsafety_true-termination.c, 51393d639f010eae1b63625f7a13f75512f9f6892d9718dd03fa54720c8c54a0
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/51393d639f010eae1b63625f7a13f75512f9f6892d9718dd03fa54720c8c54a0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
890707c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 3 | 2019-12-01T01:52:56+01:00 | ||
e0f4422 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 3 | 2019-11-29T23:12:49+01:00 |
Found 4 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero3_true-valid-memsafety_true-termination.c, 51393d639f010eae1b63625f7a13f75512f9f6892d9718dd03fa54720c8c54a0
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/51393d639f010eae1b63625f7a13f75512f9f6892d9718dd03fa54720c8c54a0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
19793f8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T09:51 CET (sv-comp) | ||
68856e9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 3 | 2018-12-07T13:13:57+01:00 | ||
31be724 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-05T21:13:21+01:00 | ||
55d4101 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T04:11 CET (sv-comp) |
Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero3_true-valid-memsafety_true-termination.c, 51393d639f010eae1b63625f7a13f75512f9f6892d9718dd03fa54720c8c54a0
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/51393d639f010eae1b63625f7a13f75512f9f6892d9718dd03fa54720c8c54a0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
10cb037 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T23:30 CET (sv-comp) | ||
85e3a10 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 3 | 2017-12-01T08:24:22+01:00 | ||
7037735 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T11:14:20.328302 | ||
d17e7ed | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T23:18:43.811706 | ||
3dc1b0b | 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-03T07:00Z | ||
54b794b | 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:40 CET (sv-comp) | ||
98a46ab | 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-03T03:56Z | ||
82fb52b | 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:26 CET (sv-comp) | ||
9f96690 | 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:58Z | ||
4ca7884 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-01T09:25:16+01:00 | ||
2323bc5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T20:13:12.513783 | ||
df19245 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T07:45:39.060423 | ||
0a520f1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 5 | 2017-12-01T17:23 CET (sv-comp) | ||
87ecae1 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 4 | 2017-12-01T15:14 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero3_true-valid-memsafety_true-termination.c, 51393d639f010eae1b63625f7a13f75512f9f6892d9718dd03fa54720c8c54a0
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/51393d639f010eae1b63625f7a13f75512f9f6892d9718dd03fa54720c8c54a0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |