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 14 witnesses for program sv-benchmarks/c/pthread-memsafety/fillarray1_false-valid-deref.i, 0d955c319d131d508b8618ef571ba23da865842e29989ccda626762130a6dda2
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/0d955c319d131d508b8618ef571ba23da865842e29989ccda626762130a6dda2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
10fc955 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T10:54:20+01:00 | ||
57e2797 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-18T12:01:14+01:00 | 10fc955 | |
8c741ea | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-04T12:12:36+01:00 | 4a9939c | |
4f80967 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-01T18:27:11+01:00 | 86138e3 | |
3657e80 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-11-30T05:37:31+01:00 | ||
1321ce9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-11-29T08:32:50+01:00 | f9a7b2b | |
04018ec | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-11-28T23:49:53+01:00 | 0b1f616 | |
50e16b5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 4 | 2023-12-04T00:14:19+01:00 | ||
e0ffb35 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 6 | 2023-12-18T01:59:06+01:00 | ||
86138e3 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.4.0 incr | 4 | 2023-12-01T14:00:07Z | ||
4a9939c | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Taipan | 10 | 2023-12-02T17:08:20Z | ||
f9a7b2b | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Automizer | 10 | 2023-11-29T01:42:12Z | ||
0b1f616 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | sv-sanitizers 0.1.1 | 3 | 2023-11-28T19:55:42Z | ||
5f81c69 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 4 | 2023-12-18T20:16:07+01:00 |
Found 14 witnesses for program sv-benchmarks/c/pthread-memsafety/fillarray1_false-valid-deref.i, 0d955c319d131d508b8618ef571ba23da865842e29989ccda626762130a6dda2
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/0d955c319d131d508b8618ef571ba23da865842e29989ccda626762130a6dda2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
eb67448 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T07:06:47+01:00 | ||
9553cc3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T10:43:17+01:00 | 506c811 | |
8b8765d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T06:53:13+01:00 | 40b209d | |
b709bc8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T15:42:06+01:00 | 3f15b71 | |
e2c10b8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T14:17:38+01:00 | eb67448 | |
3e1dea8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T02:25:10+01:00 | 4ecdfe5 | |
c3899a4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 4 | 2022-12-10T19:24:15+01:00 | ||
089cce3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 4 | 2022-12-11T21:23:45+01:00 | ||
320ebce | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 4 | 2022-12-09T16:56:13+01:00 | ||
efae7d4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 6 | 2022-12-09T02:39:40+01:00 | ||
3f15b71 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 4 | 2022-12-18T19:23:47Z | ||
4ecdfe5 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2022-12-25T09:16:28Z | ||
506c811 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Taipan | 10 | 2022-12-14T06:17:36Z | ||
40b209d | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Automizer | 10 | 2022-12-13T19:08:03Z |
Found 15 witnesses for program sv-benchmarks/c/pthread-memsafety/fillarray1_false-valid-deref.i, 0d955c319d131d508b8618ef571ba23da865842e29989ccda626762130a6dda2
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/0d955c319d131d508b8618ef571ba23da865842e29989ccda626762130a6dda2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ebea5ff | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T09:20:53+01:00 | ||
8dec45b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-10T08:34:11+01:00 | 7a49659 | |
f715041 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-08T13:50:02+01:00 | a3025f6 | |
27030f8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-07T11:27:27+01:00 | ebea5ff | |
5183b95 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-07T02:35:39+01:00 | e0b2123 | |
e174b5d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-06T12:47:33+01:00 | 875eba6 | |
95c0bdf | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-05T18:02:15+01:00 | ||
2f94d00 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 4 | 2021-12-10T18:12:25+01:00 | ||
25642de | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 6 | 2021-12-07T02:08:21+01:00 | ||
a3025f6 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2021-12-08T08:37:04Z | ||
01c831e | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 4 | 2021-12-09T10:33:01+01:00 | ||
7a49659 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Taipan | 10 | 2021-12-09T23:08:54Z | ||
e0b2123 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Automizer | 10 | 2021-12-06T23:42:21Z | ||
875eba6 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | SESL | 3 | 2021-12-06T12:12:04+01:00 | ||
06e07f4 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 4 | 2021-12-08T16:55:59+01:00 |
Found 6 witnesses for program sv-benchmarks/c/pthread-memsafety/fillarray1_false-valid-deref.i, 0d955c319d131d508b8618ef571ba23da865842e29989ccda626762130a6dda2
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/0d955c319d131d508b8618ef571ba23da865842e29989ccda626762130a6dda2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a8ac3cd | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T12:46:05+01:00 | ||
4764e34 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-09T21:39:09+01:00 | 47546d5 | |
6108dd4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-07T16:09:17+01:00 | 505c5f8 | |
ed20c7a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-06T19:32:17+01:00 | a8ac3cd | |
8ab52ce | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-05T16:14:14+01:00 | ||
60514a6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 4 | 2020-12-07T23:43:18+01:00 |
Found 6 witnesses for program sv-benchmarks/c/pthread-memsafety/fillarray1_false-valid-deref.i, 0d955c319d131d508b8618ef571ba23da865842e29989ccda626762130a6dda2
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/0d955c319d131d508b8618ef571ba23da865842e29989ccda626762130a6dda2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c9aa1af | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 4 | 2019-12-11T21:44:10+01:00 | bd17b1f | |
e8d00ee | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 4 | 2019-11-30T04:01:16+01:00 | ||
7f530af | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 4 | 2019-12-11T20:54:21+01:00 | 62efddd | |
275e4d5 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 4 | 2019-12-08T00:27:02+01:00 | f769833 | |
1a0931e | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 4 | 2019-12-03T08:10:17+01:00 | e8d00ee | |
bd17b1f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 4 | 2019-12-01T01:39:07+01:00 |
Found 6 witnesses for program sv-benchmarks/c/pthread-memsafety/fillarray1_false-valid-deref.i, 0d955c319d131d508b8618ef571ba23da865842e29989ccda626762130a6dda2
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/0d955c319d131d508b8618ef571ba23da865842e29989ccda626762130a6dda2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
25e608d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 4 | 2018-12-07T08:59:39+01:00 | ||
8eaf750 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-09T20:53:11+01:00 | 76feebc | |
66185fd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T10:18:29+01:00 | 9a14b7d | |
ea6b778 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T04:59:01+01:00 | c109ab4 | |
15703e1 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T09:17:36+01:00 | 7d7632d | |
c8820f7 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-05T10:49:17+01:00 |
Found 0 witnesses for program sv-benchmarks/c/pthread-memsafety/fillarray1_false-valid-deref.i, 0d955c319d131d508b8618ef571ba23da865842e29989ccda626762130a6dda2
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/0d955c319d131d508b8618ef571ba23da865842e29989ccda626762130a6dda2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/pthread-memsafety/fillarray1_false-valid-deref.i, 0d955c319d131d508b8618ef571ba23da865842e29989ccda626762130a6dda2
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/0d955c319d131d508b8618ef571ba23da865842e29989ccda626762130a6dda2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |