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/sep05_true-unreach-call_true-termination.i |
programSHA | 34eefd001a517b6e61aa5789838c2deceedf4325faa7eb36bdf2db0f42046ced |
witnessName | results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.sep05_true-unreach-call_true-termination.i.files/witness.graphml |
witnessSHA | 9a7394341967d3aeab21ffe9098de4965cff4bf21f71b08dacbfd8c4d63240f8 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-03T02:04:52+01:00 |
producer | CPAchecker 1.6.1-svn |
program-sha256 | 34eefd001a517b6e61aa5789838c2deceedf4325faa7eb36bdf2db0f42046ced |
programfile | /home/benchexec/ar_abs_temp/sep05_true_unreach_call_true_termination.c |
programhash | d0de1e24b39a951a670bac9cdad830e10aacf376 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/9a7394341967d3aeab21ffe9098de4965cff4bf21f71b08dacbfd8c4d63240f8.graphml |
witness-sha256 | 9a7394341967d3aeab21ffe9098de4965cff4bf21f71b08dacbfd8c4d63240f8 |
witness-size | 22602 |
witness-type | correctness_witness |
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/sep05_true-unreach-call_true-termination.i, 34eefd001a517b6e61aa5789838c2deceedf4325faa7eb36bdf2db0f42046ced
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/34eefd001a517b6e61aa5789838c2deceedf4325faa7eb36bdf2db0f42046ced.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/sep05_true-unreach-call_true-termination.i, 34eefd001a517b6e61aa5789838c2deceedf4325faa7eb36bdf2db0f42046ced
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/34eefd001a517b6e61aa5789838c2deceedf4325faa7eb36bdf2db0f42046ced.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/sep05_true-unreach-call_true-termination.i, 34eefd001a517b6e61aa5789838c2deceedf4325faa7eb36bdf2db0f42046ced
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/34eefd001a517b6e61aa5789838c2deceedf4325faa7eb36bdf2db0f42046ced.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/sep05_true-unreach-call_true-termination.i, 34eefd001a517b6e61aa5789838c2deceedf4325faa7eb36bdf2db0f42046ced
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/34eefd001a517b6e61aa5789838c2deceedf4325faa7eb36bdf2db0f42046ced.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 11 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/sep05_true-unreach-call_true-termination.i, 34eefd001a517b6e61aa5789838c2deceedf4325faa7eb36bdf2db0f42046ced
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/34eefd001a517b6e61aa5789838c2deceedf4325faa7eb36bdf2db0f42046ced.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c43b9b1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:34 CET (comp) | ||
f477942 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T20:19:08+01:00 | 6f2897b | |
5bd4cdf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T20:02:16+01:00 | fbddf71 | |
e85ad34 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-08T00:37:18+01:00 | 243915f | |
956197c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-06T02:18:16+01:00 | 8e8894c | |
fc2a588 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-05T19:12:47+01:00 | 1992054 | |
843de67 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-04T02:07:48+01:00 | c43b9b1 | |
21cf7a3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-11-30T19:54:39+01:00 | 738914e | |
1d2cfd4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-11-30T17:28:03+01:00 | 795281e | |
795281e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 33 | 2019-11-29T22:55:24+01:00 | ||
c4d6be5 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-03T21:45 CET (comp) |
Found 19 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/sep05_true-unreach-call_true-termination.i, 34eefd001a517b6e61aa5789838c2deceedf4325faa7eb36bdf2db0f42046ced
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/34eefd001a517b6e61aa5789838c2deceedf4325faa7eb36bdf2db0f42046ced.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
282b433 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T00:18 CET (sv-comp) | ||
7933e4d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T07:15:37 | ||
4bf9381 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T06:33 CET (sv-comp) | ||
e4b5bf5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 10 | 2018-12-07T01:45:37+01:00 | ||
5b6bf4e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-10T19:45:50+01:00 | 1f79556 | |
051f9c4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-09T21:12:31+01:00 | d77e712 | |
dc3861a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T23:14:09+01:00 | 282b433 | |
0bdc521 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T21:54:17+01:00 | 7933e4d | |
cfb73e9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T06:05:09+01:00 | e4b5bf5 | |
f36d88a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T02:29:01+01:00 | 9526d81 | |
ef908fe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T01:53:11+01:00 | bb2965d | |
49ab64f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-07T17:51:49+01:00 | 2908a3b | |
e0b63ec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-07T16:44:27+01:00 | 4bf9381 | |
299ac0a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T09:35:20+01:00 | 9f70af8 | |
8882b14 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T08:47:03+01:00 | ce985ae | |
be7a4c9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T08:29:49+01:00 | 3ca7d48 | |
ce985ae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 33 | 2018-12-05T20:37:15+01:00 | ||
65a9f80 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T06:10 CET (sv-comp) | ||
d9ad3c8 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T04:06 CET (sv-comp) |
Found 28 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/sep05_true-unreach-call_true-termination.i, 34eefd001a517b6e61aa5789838c2deceedf4325faa7eb36bdf2db0f42046ced
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/34eefd001a517b6e61aa5789838c2deceedf4325faa7eb36bdf2db0f42046ced.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8fa80ff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 62 | 2017-12-01T03:10:44+01:00 | ||
a76db4b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 34 | 2017-11-30T15:02:47+01:00 | ||
2908a3b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T22:27 CET (sv-comp) | ||
e5ef44e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T18:22 CET (sv-comp) | ||
ff7e2e2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Map2Check | 5 | 2017-12-01T21:16 CET (sv-comp) | ||
33ae7ec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T01:49:37.820874 | ||
7ea9f86 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T14:53:29.870420 | ||
c148f1e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T01:41:49.994543 | ||
1a7b6cb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T08:57:51.578106 | ||
1c7e21d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 18 | 2017-12-01T15:50 CET (sv-comp) | ||
9a73943 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 23 | 2017-12-03T02:04:52+01:00 | ||
f19c1e8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 24 | 2017-11-30T20:09:14+01:00 | ||
b013aa9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-02T20:44:19+01:00 | ba05780 | |
5c9ff03 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-02T15:09:15+01:00 | df6fb55 | |
d9df455 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-02T09:00:57+01:00 | c7e5fa4 | |
b7e7ea6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-02T00:19:06+01:00 | 77d4c23 | |
6dd5dc8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T22:46:08+01:00 | 5df1b1a | |
14662d9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T22:32:12+01:00 | cbc5ec9 | |
91bcccf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T08:27:39+01:00 | fd69ae6 | |
4f6d95b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T07:16:40+01:00 | 1a3bb6e | |
f159643 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T06:02:53+01:00 | d49db9c | |
bc77f40 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T06:00:33+01:00 | 286f8c2 | |
fb848bd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-11-30T23:43:17+01:00 | ||
718b7df | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 9 | 2017-12-01T22:11:44+01:00 | ||
c72b7b6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 36 | 2017-11-30T12:24 CET (sv-comp) | ||
0c394ce | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 71 | 2017-11-30T19:22 CET (sv-comp) | ||
c839f1c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 36 | 2017-12-01T13:39 CET (sv-comp) | ||
46646cd | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 29 | 2017-12-01T12:44 CET (sv-comp) |
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/reducercommutativity/sep05_true-unreach-call_true-termination.i, 34eefd001a517b6e61aa5789838c2deceedf4325faa7eb36bdf2db0f42046ced
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/34eefd001a517b6e61aa5789838c2deceedf4325faa7eb36bdf2db0f42046ced.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |