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 | ../../../comp/sv-benchmarks/c/reducercommutativity/avg10_true-unreach-call_true-termination.i |
programSHA | 3abe92c041c76b94dad5b94ee5250254369ae5e69c8a16a44f975cb74acd5afa |
witnessName | results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.avg10_true-unreach-call_true-termination.i.files/witness.graphml |
witnessSHA | cca0faf9baaa8d72855da3fc0cee91afdb24cf9d72270e57e791fa575c8feb1c |
Key | Value |
architecture | 32bit |
creationtime | 2017-11-02T13:16:17+05:30 |
producer | CPAchecker 1.6.12-svcomp17 |
program-sha256 | 3abe92c041c76b94dad5b94ee5250254369ae5e69c8a16a44f975cb74acd5afa |
programfile | /home/benchexec/ar_abs_temp/avg10_true_unreach_call_true_termination.c |
programhash | 9f07a48114771d824f096049259b31d59f0e2427 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/cca0faf9baaa8d72855da3fc0cee91afdb24cf9d72270e57e791fa575c8feb1c.graphml |
witness-sha256 | cca0faf9baaa8d72855da3fc0cee91afdb24cf9d72270e57e791fa575c8feb1c |
witness-size | 3762 |
witness-type | correctness_witness |
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/avg10_true-unreach-call_true-termination.i, 3abe92c041c76b94dad5b94ee5250254369ae5e69c8a16a44f975cb74acd5afa
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/3abe92c041c76b94dad5b94ee5250254369ae5e69c8a16a44f975cb74acd5afa.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/avg10_true-unreach-call_true-termination.i, 3abe92c041c76b94dad5b94ee5250254369ae5e69c8a16a44f975cb74acd5afa
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/3abe92c041c76b94dad5b94ee5250254369ae5e69c8a16a44f975cb74acd5afa.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/avg10_true-unreach-call_true-termination.i, 3abe92c041c76b94dad5b94ee5250254369ae5e69c8a16a44f975cb74acd5afa
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/3abe92c041c76b94dad5b94ee5250254369ae5e69c8a16a44f975cb74acd5afa.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/avg10_true-unreach-call_true-termination.i, 3abe92c041c76b94dad5b94ee5250254369ae5e69c8a16a44f975cb74acd5afa
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/3abe92c041c76b94dad5b94ee5250254369ae5e69c8a16a44f975cb74acd5afa.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 10 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/avg10_true-unreach-call_true-termination.i, 3abe92c041c76b94dad5b94ee5250254369ae5e69c8a16a44f975cb74acd5afa
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/3abe92c041c76b94dad5b94ee5250254369ae5e69c8a16a44f975cb74acd5afa.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
de5f1ae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:40 CET (comp) | ||
dccc8ff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-12-11T20:13:06+01:00 | 1bd7108 | |
d4f4ff3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-12-11T20:03:13+01:00 | e8db1d8 | |
bacdb20 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-12-08T00:52:07+01:00 | 5232919 | |
35a5254 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-12-06T02:16:06+01:00 | aa40f3b | |
d02c5c2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-12-04T02:07:42+01:00 | de5f1ae | |
34419ed | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-11-30T19:54:59+01:00 | 18c5b96 | |
a66a0e7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-11-30T17:04:04+01:00 | 2130d34 | |
2130d34 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 12 | 2019-11-30T07:37:48+01:00 | ||
258d1cc | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:28 CET (comp) |
Found 18 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/avg10_true-unreach-call_true-termination.i, 3abe92c041c76b94dad5b94ee5250254369ae5e69c8a16a44f975cb74acd5afa
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/3abe92c041c76b94dad5b94ee5250254369ae5e69c8a16a44f975cb74acd5afa.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9181281 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T02:53 CET (sv-comp) | ||
4877c3b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T00:12:08 | ||
9301ce1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-06T20:25 CET (sv-comp) | ||
c4c6039 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 12 | 2018-12-07T19:23:02+01:00 | ||
6e1c05a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-10T20:21:34+01:00 | a01dc12 | |
ec323bf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-09T21:21:23+01:00 | 3c2e5aa | |
bd60bdf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T23:22:07+01:00 | 9181281 | |
07ab653 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T21:38:12+01:00 | 4877c3b | |
919bd19 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T06:26:18+01:00 | c4c6039 | |
e57573a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T04:34:01+01:00 | 8705370 | |
8758a7e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T02:45:06+01:00 | 6403448 | |
9013c2b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-07T17:58:57+01:00 | da82c10 | |
40e6451 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-07T16:52:29+01:00 | 9301ce1 | |
40ed0f5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T09:43:36+01:00 | a3aee3b | |
3aef12a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T09:26:19+01:00 | b1d8f0f | |
b1d8f0f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-06T01:26:50+01:00 | ||
be718ea | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T19:09 CET (sv-comp) | ||
81860d6 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T01:45 CET (sv-comp) |
Found 22 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/avg10_true-unreach-call_true-termination.i, 3abe92c041c76b94dad5b94ee5250254369ae5e69c8a16a44f975cb74acd5afa
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/3abe92c041c76b94dad5b94ee5250254369ae5e69c8a16a44f975cb74acd5afa.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f47d022 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 95 | 2017-12-01T02:55:24+01:00 | ||
278951f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 46 | 2017-12-01T03:03:40+01:00 | ||
8e605e9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 16 | 2017-12-01T22:45:29+01:00 | ||
da82c10 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T23:14 CET (sv-comp) | ||
e2ca720 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T17:10 CET (sv-comp) | ||
af9c493 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T01:57:24.585092 | ||
bd06b44 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T11:36:48.245040 | ||
c53b2e4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T22:11:50.112041 | ||
b542438 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T08:32:35.271802 | ||
aee0f53 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 17 | 2017-12-01T19:06 CET (sv-comp) | ||
fe9a711 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 17 | 2017-12-01T01:17 CET (sv-comp) | ||
cca0faf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.12-svcomp17 | 4 | 2017-11-02T13:16:17+05:30 | ||
8397aa4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-12-03T04:16:47+01:00 | f7ff675 | |
b16269c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-12-02T20:54:44+01:00 | 6cdd294 | |
592ad28 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-12-02T08:33:26+01:00 | 900f92b | |
48cfc93 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-12-02T00:31:33+01:00 | c1a690b | |
d1f1e5a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-12-01T22:44:33+01:00 | 8c12864 | |
75924dc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-12-01T08:28:48+01:00 | f7626f0 | |
5c1ad60 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-12-01T06:03:15+01:00 | 23960c8 | |
b0a36fb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 46 | 2017-11-30T11:34 CET (sv-comp) | ||
61f67a5 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 45 | 2017-12-01T16:44 CET (sv-comp) | ||
a17693a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 26 | 2017-12-01T15:10 CET (sv-comp) |
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/avg10_true-unreach-call_true-termination.i, 3abe92c041c76b94dad5b94ee5250254369ae5e69c8a16a44f975cb74acd5afa
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/3abe92c041c76b94dad5b94ee5250254369ae5e69c8a16a44f975cb74acd5afa.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |