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).
Key | Value |
programName | sv-benchmarks/c/reducercommutativity/avg05_true-unreach-call_true-termination.i |
programSHA | 29e94c0fc6eb8325839be9d29c45d81073b114623b0a8f335323793ef79ca0ad |
witnessName | results-verified/viap.2018-12-09_1849.logfiles/sv-comp19_prop-reachsafety.avg05_true-unreach-call_true-termination.i.files/witness.graphml |
witnessSHA | abc285b25c65f87de1c9605cd9b61adf9da29a687e33397b6535d919a3aa85d0 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-09T18:57 CET (sv-comp) |
memorymodel | precise |
producer | VIAP |
programfile | ../../sv-benchmarks/c/reducercommutativity/avg05_true-unreach-call_true-termination.i |
programhash | 3cd0186843eb184a03f25fecfe7ca0b9c84c33a9 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/abc285b25c65f87de1c9605cd9b61adf9da29a687e33397b6535d919a3aa85d0.graphml |
witness-sha256 | abc285b25c65f87de1c9605cd9b61adf9da29a687e33397b6535d919a3aa85d0 |
witness-size | 3581 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/avg05_true-unreach-call_true-termination.i, 29e94c0fc6eb8325839be9d29c45d81073b114623b0a8f335323793ef79ca0ad
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/29e94c0fc6eb8325839be9d29c45d81073b114623b0a8f335323793ef79ca0ad.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/avg05_true-unreach-call_true-termination.i, 29e94c0fc6eb8325839be9d29c45d81073b114623b0a8f335323793ef79ca0ad
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/29e94c0fc6eb8325839be9d29c45d81073b114623b0a8f335323793ef79ca0ad.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/avg05_true-unreach-call_true-termination.i, 29e94c0fc6eb8325839be9d29c45d81073b114623b0a8f335323793ef79ca0ad
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/29e94c0fc6eb8325839be9d29c45d81073b114623b0a8f335323793ef79ca0ad.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/avg05_true-unreach-call_true-termination.i, 29e94c0fc6eb8325839be9d29c45d81073b114623b0a8f335323793ef79ca0ad
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/29e94c0fc6eb8325839be9d29c45d81073b114623b0a8f335323793ef79ca0ad.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 10 witnesses for program sv-benchmarks/c/reducercommutativity/avg05_true-unreach-call_true-termination.i, 29e94c0fc6eb8325839be9d29c45d81073b114623b0a8f335323793ef79ca0ad
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/29e94c0fc6eb8325839be9d29c45d81073b114623b0a8f335323793ef79ca0ad.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4565ec7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:52 CET (comp) | ||
745c5c5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-12-11T20:14:33+01:00 | 16e5658 | |
4d1fccb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-12-11T20:02:40+01:00 | 9e3066f | |
89ad49d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-12-08T00:36:22+01:00 | 138a6b3 | |
625ef28 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-12-06T02:20:21+01:00 | e43850f | |
c4d0e2e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-12-04T02:07:26+01:00 | 4565ec7 | |
f841977 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-11-30T19:56:03+01:00 | 7af04f8 | |
2e5b4ec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-11-30T17:01:48+01:00 | b2dcf57 | |
b2dcf57 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 11 | 2019-11-29T18:46:05+01:00 | ||
dacc991 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:37 CET (comp) |
Found 19 witnesses for program sv-benchmarks/c/reducercommutativity/avg05_true-unreach-call_true-termination.i, 29e94c0fc6eb8325839be9d29c45d81073b114623b0a8f335323793ef79ca0ad
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/29e94c0fc6eb8325839be9d29c45d81073b114623b0a8f335323793ef79ca0ad.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f3ea128 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T11:59 CET (sv-comp) | ||
7bec9cd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T17:13:09 | ||
923c5d8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T08:21 CET (sv-comp) | ||
b6a4275 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 11 | 2018-12-07T15:27:45+01:00 | ||
6252624 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-10T20:32:06+01:00 | ecebac1 | |
a3c626c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-09T21:21:35+01:00 | abc285b | |
645bb81 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-09T20:08:49+01:00 | 525fe30 | |
ae50a8e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T23:24:50+01:00 | f3ea128 | |
59ed993 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T21:31:49+01:00 | 7bec9cd | |
5cc79dc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T06:48:03+01:00 | b6a4275 | |
a9cc300 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T03:22:40+01:00 | 1ec9220 | |
8f96755 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T02:35:06+01:00 | 0c91908 | |
9155013 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-07T17:58:32+01:00 | b4ba68d | |
61962c0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-07T16:52:34+01:00 | 923c5d8 | |
a012162 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T09:43:09+01:00 | 911b3b6 | |
4c273ee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T09:17:04+01:00 | 7a29e0d | |
7a29e0d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 11 | 2018-12-06T07:38:22+01:00 | ||
30c7b3b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T10:11 CET (sv-comp) | ||
659e5f8 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T06:43 CET (sv-comp) |
Found 25 witnesses for program sv-benchmarks/c/reducercommutativity/avg05_true-unreach-call_true-termination.i, 29e94c0fc6eb8325839be9d29c45d81073b114623b0a8f335323793ef79ca0ad
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/29e94c0fc6eb8325839be9d29c45d81073b114623b0a8f335323793ef79ca0ad.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
253fd8e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 58 | 2017-12-01T01:55:27+01:00 | ||
4b181b3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 27 | 2017-11-30T11:53:06+01:00 | ||
24dc558 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 11 | 2017-12-02T02:16:54+01:00 | ||
b4ba68d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T22:14 CET (sv-comp) | ||
01a50c2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T09:37 CET (sv-comp) | ||
b54439a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Map2Check | 5 | 2017-12-01T21:39 CET (sv-comp) | ||
6b8ce39 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T00:22:25.851571 | ||
0b656e1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T13:40:32.566674 | ||
4278c82 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T16:52:08.413623 | ||
2e62d0f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T20:59:29.890419 | ||
cf9d267 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 11 | 2017-12-01T18:54 CET (sv-comp) | ||
5da8909 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 11 | 2017-12-01T02:25 CET (sv-comp) | ||
d1e3449 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.12-svcomp17 | 4 | 2017-11-02T13:16:17+05:30 | ||
5805909 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-12-03T04:36:45+01:00 | e08652e | |
0b9fcba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-12-02T20:34:06+01:00 | d38cbd3 | |
681efa6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-12-02T07:35:44+01:00 | 18dc804 | |
d6f239f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-12-02T00:28:49+01:00 | 648c8b1 | |
4ed73b5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-12-01T22:41:20+01:00 | 27ff4fb | |
a082064 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-12-01T22:34:20+01:00 | 2a487fd | |
1561668 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-12-01T08:28:42+01:00 | 662505e | |
a9edba2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T05:28:25+01:00 | 2effc58 | |
ac7e7a0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 28 | 2017-11-30T15:56 CET (sv-comp) | ||
fffd882 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 54 | 2017-11-30T13:02 CET (sv-comp) | ||
756383e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 28 | 2017-12-01T16:47 CET (sv-comp) | ||
4157a0c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 26 | 2017-12-01T17:03 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/reducercommutativity/avg05_true-unreach-call_true-termination.i, 29e94c0fc6eb8325839be9d29c45d81073b114623b0a8f335323793ef79ca0ad
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/29e94c0fc6eb8325839be9d29c45d81073b114623b0a8f335323793ef79ca0ad.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |