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 sv-benchmarks/c/ldv-memsafety/memset2_true-valid-memsafety_true-termination.c, feb75add31ebc5ab880174a59d6376758f323c6b10b547c6921a4d0c74b13daf
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/feb75add31ebc5ab880174a59d6376758f323c6b10b547c6921a4d0c74b13daf.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1d055ba | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T08:04:11+01:00 | ||
0f048ab | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T19:16:57Z | ||
30e11d8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-18T12:01:02+01:00 | 1d055ba | |
d78e8fd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-11-30T02:22:04+01:00 | ||
aa55871 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 3 | 2023-12-03T23:41:48+01:00 | ||
aef93e2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2023-12-18T23:57:10+01:00 | ||
60fbf0e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2023-12-18T02:00:13+01:00 | ||
f0de0da | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-05T08:56:57Z | ||
e83a8cb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-04T14:34:11Z | ||
dcb2cf9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-01T19:58:29Z | ||
de42dd7 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.4.0 incr | 3 | 2023-12-01T13:01:18Z | ||
d4b2475 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0 | 3 | 2023-12-19T13:13:02+01:00 | ||
7f823d0 | 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-02T18:29:39Z | ||
69e069f | 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:14Z | ||
654e20f | 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-29T11:57:23Z | ||
df33be7 | 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:07:09Z | ||
35a703c | 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:52:12Z | ||
c7d7592 | 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-17T11:11:07+01:00 | ||
2936de6 | 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:38:58Z | ||
405d4e7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.4.0 | 3 | 2023-12-01T10:41:32Z | ||
ba63849 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T23:56:45Z | ||
565327f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 3 | 2023-12-01T01:02:12Z | ||
10e2d84 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 3 | 2023-12-17T09:09:32+01:00 | ||
d0c7ab2 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-05T08:26:48Z | ||
87935e8 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-04T09:45:29Z | ||
0cd0a92 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2023-12-01T20:52:42Z |
Found 20 witnesses for program sv-benchmarks/c/ldv-memsafety/memset2_true-valid-memsafety_true-termination.c, feb75add31ebc5ab880174a59d6376758f323c6b10b547c6921a4d0c74b13daf
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/feb75add31ebc5ab880174a59d6376758f323c6b10b547c6921a4d0c74b13daf.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6589599 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:48:48+01:00 | ||
370d3b8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-28T14:14:19+01:00 | 6589599 | |
5050143 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2022-12-10T17:34:57+01:00 | ||
1f3b173 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 3 | 2022-12-11T20:32:45+01:00 | ||
d67027a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2022-12-09T02:56:04+01:00 | ||
71e9c4b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2022-12-08T17:12:57Z | ||
c38c484 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 7.0.0 incr | 3 | 2022-12-18T18:49:51Z | ||
0a2d26a | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2022-12-25T10:00:55Z | ||
833bb00 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2022-12-10T02:01:01+01:00 | ||
411db9f | 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-14T07:51:42Z | ||
a17dad4 | 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:06Z | ||
f63b342 | 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 | 2022-12-15T01:52:55Z | ||
4a1e6e6 | 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-08T09:34:30+01:00 | ||
5c577cf | 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-13T21:14:49Z | ||
098e0c3 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0 | 3 | 2022-12-11T05:48:28+01:00 | ||
b9dd966 | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2022-12-25T12:11:37Z | ||
572ea9c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 7.0.0 | 3 | 2022-12-18T16:28:08Z | ||
bce9a6e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T16:43:05Z | ||
7fd5a81 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 3 | 2022-12-08T11:10:03+01:00 | ||
6574813 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 2 | 2022-12-08T21:06:20Z |
Found 13 witnesses for program sv-benchmarks/c/ldv-memsafety/memset2_true-valid-memsafety_true-termination.c, feb75add31ebc5ab880174a59d6376758f323c6b10b547c6921a4d0c74b13daf
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/feb75add31ebc5ab880174a59d6376758f323c6b10b547c6921a4d0c74b13daf.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2cc6cd5 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T09:32:57+01:00 | ||
9a9062d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-05T17:28:17+01:00 | ||
c6482cd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2021-12-09T11:43:15+01:00 | ||
0971fbf | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2021-12-07T03:36:36+01:00 | ||
ce65f11 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 6.8.0 incr | 3 | 2021-12-08T11:07:12Z | ||
fcdb07d | 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-10T05:18:06Z | ||
e17a594 | 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 | 2021-12-10T14:26:56Z | ||
38c9b04 | 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-06T09:50:27+01:00 | ||
7af82c4 | 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:26:28Z | ||
2f42799 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 3 | 2021-12-08T19:33:55+01:00 | ||
506518f | Inspect | CHECK( init(main()), LTL(G ! call(reach_error())) ) | correctness_witness | ESBMC 6.8.0 | 3 | 2021-12-08T03:44:54Z | ||
44a50e3 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2021-12-07T13:34:25Z | ||
240b8bb | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 3 | 2021-12-06T03:46:21+01:00 |
Found 5 witnesses for program sv-benchmarks/c/ldv-memsafety/memset2_true-valid-memsafety_true-termination.c, feb75add31ebc5ab880174a59d6376758f323c6b10b547c6921a4d0c74b13daf
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/feb75add31ebc5ab880174a59d6376758f323c6b10b547c6921a4d0c74b13daf.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e0fe8a1 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T17:59:20+01:00 | ||
b1e4deb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 3 | 2020-12-05T13:44:48+01:00 | ||
2e6d79d | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2020-12-08T04:03:44+01:00 | ||
84d91a4 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T21:39:53 | ||
bec3bac | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T22:28:52 |
Found 2 witnesses for program sv-benchmarks/c/ldv-memsafety/memset2_true-valid-memsafety_true-termination.c, feb75add31ebc5ab880174a59d6376758f323c6b10b547c6921a4d0c74b13daf
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/feb75add31ebc5ab880174a59d6376758f323c6b10b547c6921a4d0c74b13daf.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
25f381a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 3 | 2019-11-29T16:17:18+01:00 | ||
7461519 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 3 | 2019-12-01T08:43:28+01:00 |
Found 4 witnesses for program sv-benchmarks/c/ldv-memsafety/memset2_true-valid-memsafety_true-termination.c, feb75add31ebc5ab880174a59d6376758f323c6b10b547c6921a4d0c74b13daf
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/feb75add31ebc5ab880174a59d6376758f323c6b10b547c6921a4d0c74b13daf.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c9457c3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T19:20 CET (sv-comp) | ||
84e2b96 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-05T17:27:58+01:00 | ||
cce6ed5 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 3 | 2018-12-07T10:15:29+01:00 | ||
4f2783d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T09:31 CET (sv-comp) |
Found 15 witnesses for program sv-benchmarks/c/ldv-memsafety/memset2_true-valid-memsafety_true-termination.c, feb75add31ebc5ab880174a59d6376758f323c6b10b547c6921a4d0c74b13daf
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/feb75add31ebc5ab880174a59d6376758f323c6b10b547c6921a4d0c74b13daf.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e98709f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T23:14 CET (sv-comp) | ||
40cb50b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-01T09:36:21+01:00 | ||
9662dce | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T11:36:53.639365 | ||
2a2aa60 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T23:23:26.521479 | ||
5763a21 | 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:01Z | ||
9fe701c | 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:37 CET (sv-comp) | ||
600f29c | 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:48Z | ||
77a3587 | 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:30 CET (sv-comp) | ||
4315d42 | 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 | 2017-12-01T08:26 CET (sv-comp) | ||
eb937a9 | 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:28Z | ||
910ae64 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 3 | 2017-12-01T08:34:16+01:00 | ||
695aeb8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T22:38:24.206335 | ||
122c838 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T15:37:44.733911 | ||
ca9c70b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 5 | 2017-12-01T19:28 CET (sv-comp) | ||
a61c5fe | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 3 | 2017-12-01T18:03 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memset2_true-valid-memsafety_true-termination.c, feb75add31ebc5ab880174a59d6376758f323c6b10b547c6921a4d0c74b13daf
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/feb75add31ebc5ab880174a59d6376758f323c6b10b547c6921a4d0c74b13daf.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |