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 15 witnesses for program sv-benchmarks/c/pthread-memsafety/fillarray_false-valid-deref.i, 042c5199cb977bee0e9fb33f98d35f27e793036e412b430f7152f110aa730c52
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/042c5199cb977bee0e9fb33f98d35f27e793036e412b430f7152f110aa730c52.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8fa2aa5 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T08:08:58+01:00 | ||
c1c7761 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-18T12:07:56+01:00 | 8fa2aa5 | |
77521c7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-04T12:12:34+01:00 | b0ff7d2 | |
7c5cfd6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-01T18:27:23+01:00 | 43dcb7a | |
5db1fd1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-11-30T07:55:58+01:00 | ||
f459449 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-11-29T08:34:17+01:00 | 009aa94 | |
b706d2e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-11-28T23:49:42+01:00 | 4539f42 | |
d07fbe1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 4 | 2023-12-03T18:14:06+01:00 | ||
733098c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 6 | 2023-12-18T01:33:56+01:00 | ||
43dcb7a | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.4.0 incr | 4 | 2023-12-01T16:29:32Z | ||
b0ff7d2 | 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 | 8 | 2023-12-02T16:15:27Z | ||
009aa94 | 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 | 8 | 2023-11-29T01:38:12Z | ||
4539f42 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | sv-sanitizers 0.1.1 | 3 | 2023-11-28T21:49:16Z | ||
b9c712c | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0 | 4 | 2023-12-19T13:23:06+01:00 | ||
2c4f015 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 4 | 2023-12-18T21:37:28+01:00 |
Found 15 witnesses for program sv-benchmarks/c/pthread-memsafety/fillarray_false-valid-deref.i, 042c5199cb977bee0e9fb33f98d35f27e793036e412b430f7152f110aa730c52
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/042c5199cb977bee0e9fb33f98d35f27e793036e412b430f7152f110aa730c52.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1f120f1 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:31:10+01:00 | ||
c349777 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T10:44:34+01:00 | 7c4d763 | |
3d81ef9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T06:54:47+01:00 | 11ace2f | |
d27555c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T15:45:02+01:00 | 8e184f0 | |
2f54d17 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T14:21:08+01:00 | 1f120f1 | |
0da65d5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T02:24:58+01:00 | 58aadf1 | |
a1e0e0b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 4 | 2022-12-10T21:22:16+01:00 | ||
70c2df0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 4 | 2022-12-12T00:26:12+01:00 | ||
863a28e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 4 | 2022-12-11T05:46:39+01:00 | ||
027fab5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 4 | 2022-12-10T01:58:39+01:00 | ||
389e964 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 6 | 2022-12-09T03:09:48+01:00 | ||
8e184f0 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 4 | 2022-12-19T01:42:34Z | ||
58aadf1 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2022-12-25T11:51:41Z | ||
7c4d763 | 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 | 8 | 2022-12-14T04:16:05Z | ||
11ace2f | 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 | 8 | 2022-12-13T10:46:36Z |
Found 15 witnesses for program sv-benchmarks/c/pthread-memsafety/fillarray_false-valid-deref.i, 042c5199cb977bee0e9fb33f98d35f27e793036e412b430f7152f110aa730c52
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/042c5199cb977bee0e9fb33f98d35f27e793036e412b430f7152f110aa730c52.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9efb866 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T08:09:44+01:00 | ||
0564e6e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-10T08:34:13+01:00 | 4a40073 | |
fc094a0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-08T13:50:05+01:00 | 2b5426d | |
ae9655c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-07T11:27:16+01:00 | 9efb866 | |
55d2f56 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-07T02:35:08+01:00 | 1c8a6ef | |
ee86312 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-06T12:47:33+01:00 | 1932ec8 | |
080b4ec | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-05T16:13:33+01:00 | ||
b37b3f1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 4 | 2021-12-09T12:47:35+01:00 | ||
d3fec33 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 6 | 2021-12-07T01:56:38+01:00 | ||
2b5426d | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2021-12-08T04:25:03Z | ||
5469e85 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0 | 4 | 2021-12-10T19:46:28+01:00 | ||
4a40073 | 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 | 8 | 2021-12-10T00:52:53Z | ||
1c8a6ef | 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 | 8 | 2021-12-06T18:07:13Z | ||
1932ec8 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | SESL | 3 | 2021-12-06T11:28:58+01:00 | ||
3c628e0 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 4 | 2021-12-08T19:04:26+01:00 |
Found 6 witnesses for program sv-benchmarks/c/pthread-memsafety/fillarray_false-valid-deref.i, 042c5199cb977bee0e9fb33f98d35f27e793036e412b430f7152f110aa730c52
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/042c5199cb977bee0e9fb33f98d35f27e793036e412b430f7152f110aa730c52.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
0f3b064 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T17:55:06+01:00 | ||
377e2dd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-07T16:09:17+01:00 | 5b18a32 | |
a0882f7 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-09T21:28:13+01:00 | 29e4b84 | |
db6699f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-06T19:20:56+01:00 | 0f3b064 | |
dca0cc0 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-05T14:07:23+01:00 | ||
0824e9c | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 4 | 2020-12-08T03:54:38+01:00 |
Found 6 witnesses for program sv-benchmarks/c/pthread-memsafety/fillarray_false-valid-deref.i, 042c5199cb977bee0e9fb33f98d35f27e793036e412b430f7152f110aa730c52
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/042c5199cb977bee0e9fb33f98d35f27e793036e412b430f7152f110aa730c52.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9af1940 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 4 | 2019-12-08T00:27:07+01:00 | 3fa25db | |
c4f7ca7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 4 | 2019-12-03T08:08:02+01:00 | 791f01b | |
791f01b | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 4 | 2019-11-30T02:12:52+01:00 | ||
ffee236 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 4 | 2019-12-01T13:48:16+01:00 | ||
1ac8bea | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.9 | 4 | 2019-12-11T21:57:22+01:00 | ffee236 | |
b8b1a71 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.9 | 4 | 2019-12-11T20:54:28+01:00 | c7f00e8 |
Found 6 witnesses for program sv-benchmarks/c/pthread-memsafety/fillarray_false-valid-deref.i, 042c5199cb977bee0e9fb33f98d35f27e793036e412b430f7152f110aa730c52
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/042c5199cb977bee0e9fb33f98d35f27e793036e412b430f7152f110aa730c52.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f323756 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-09T20:53:21+01:00 | 30f76c4 | |
51790e8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T09:19:18+01:00 | bf5026c | |
b2176fc | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T05:04:37+01:00 | e192975 | |
5724910 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 4 | 2018-12-07T10:00:47+01:00 | ||
b64d0a2 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 |