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/recursive-simple/fibo_7_true-unreach-call_true-termination.c |
programSHA | a0bda9feccee812a2487069f4926cbe4decff2dbd38de0499ea31f5e0c23c28d |
witnessName | results-validated/cpa-seq-validate-correctness-witnesses-cbmc.2018-12-06_0735.logfiles/sv-comp19_prop-reachsafety.fibo_7_true-unreach-call_true-termination.c.files/witness.graphml |
witnessSHA | 7b0a234ef126d8521f5ca695d375713436e4d9b0ddd6139a74aa8a7355ca83d2 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-06T08:29:44+01:00 |
inputwitnesshash | 049a9c2b77cb9465474657491284bc60285b74875f0d0d8c094766a0a418994d |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | a0bda9feccee812a2487069f4926cbe4decff2dbd38de0499ea31f5e0c23c28d |
programfile | ../../sv-benchmarks/c/recursive-simple/fibo_7_true-unreach-call_true-termination.c |
programhash | a0bda9feccee812a2487069f4926cbe4decff2dbd38de0499ea31f5e0c23c28d |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/7b0a234ef126d8521f5ca695d375713436e4d9b0ddd6139a74aa8a7355ca83d2.graphml |
witness-sha256 | 7b0a234ef126d8521f5ca695d375713436e4d9b0ddd6139a74aa8a7355ca83d2 |
witness-size | 6050 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, a0bda9feccee812a2487069f4926cbe4decff2dbd38de0499ea31f5e0c23c28d).
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/fibo_7_true-unreach-call_true-termination.c, a0bda9feccee812a2487069f4926cbe4decff2dbd38de0499ea31f5e0c23c28d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/a0bda9feccee812a2487069f4926cbe4decff2dbd38de0499ea31f5e0c23c28d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/fibo_7_true-unreach-call_true-termination.c, a0bda9feccee812a2487069f4926cbe4decff2dbd38de0499ea31f5e0c23c28d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/a0bda9feccee812a2487069f4926cbe4decff2dbd38de0499ea31f5e0c23c28d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/fibo_7_true-unreach-call_true-termination.c, a0bda9feccee812a2487069f4926cbe4decff2dbd38de0499ea31f5e0c23c28d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/a0bda9feccee812a2487069f4926cbe4decff2dbd38de0499ea31f5e0c23c28d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/fibo_7_true-unreach-call_true-termination.c, a0bda9feccee812a2487069f4926cbe4decff2dbd38de0499ea31f5e0c23c28d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/a0bda9feccee812a2487069f4926cbe4decff2dbd38de0499ea31f5e0c23c28d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 15 witnesses for program sv-benchmarks/c/recursive-simple/fibo_7_true-unreach-call_true-termination.c, a0bda9feccee812a2487069f4926cbe4decff2dbd38de0499ea31f5e0c23c28d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/a0bda9feccee812a2487069f4926cbe4decff2dbd38de0499ea31f5e0c23c28d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f391086 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-03T21:46 CET (comp) | ||
3b62de0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-11T20:18:34+01:00 | fd8e615 | |
88a2f6c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-11T20:08:28+01:00 | d1db063 | |
6a26682 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-11T20:02:46+01:00 | d3324a5 | |
e0ee5b6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-08T00:52:53+01:00 | a55e38a | |
075c8d4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-07T23:20:43+01:00 | ad907a7 | |
fb5c4f3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-07T19:46:12+01:00 | 68f26d8 | |
d7d3571 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-06T02:00:47+01:00 | 834ac2b | |
c0b3d49 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-05T19:13:02+01:00 | 581324f | |
263c9af | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-04T02:07:52+01:00 | f391086 | |
90e224b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-11-30T19:27:02+01:00 | 4456e19 | |
b345941 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-11-30T16:32:08+01:00 | b3136d5 | |
b3136d5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 6 | 2019-11-30T05:35:55+01:00 | ||
d1db063 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 6 | 2019-11-30T23:34:57+01:00 | ||
f46a0cd | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:47 CET (comp) |
Found 21 witnesses for program sv-benchmarks/c/recursive-simple/fibo_7_true-unreach-call_true-termination.c, a0bda9feccee812a2487069f4926cbe4decff2dbd38de0499ea31f5e0c23c28d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/a0bda9feccee812a2487069f4926cbe4decff2dbd38de0499ea31f5e0c23c28d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a6cfae4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T01:49 CET (sv-comp) | ||
3507c42 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T03:56:22 | ||
2346fd8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T13:12 CET (sv-comp) | ||
e8c9356 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 6 | 2018-12-07T01:00:01+01:00 | ||
2c6fadc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-10T19:49:02+01:00 | c661025 | |
a099902 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-10T10:31:02+01:00 | 8bedf75 | |
32a0c32 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T21:06:38+01:00 | fcdd2e8 | |
4c245a6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T20:23:04+01:00 | 20a822e | |
a4c3a0a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T19:59:58+01:00 | 3a36675 | |
4b94996 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T23:15:32+01:00 | a6cfae4 | |
a70363b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T21:31:11+01:00 | 3507c42 | |
d9fc85a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T07:06:57+01:00 | e8c9356 | |
ed8f085 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T04:28:58+01:00 | 1c64227 | |
72e8df7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T02:27:56+01:00 | 8bedf75 | |
32bebd1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-07T16:39:32+01:00 | 2346fd8 | |
9798dac | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:29:01+01:00 | 710e13b | |
dc878e7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:01:16+01:00 | c34663d | |
7b0a234 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T08:29:44+01:00 | 049a9c2 | |
c34663d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T05:38:58+01:00 | ||
dab54c5 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T12:38 CET (sv-comp) | ||
3378c3e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T15:40 CET (sv-comp) |
Found 29 witnesses for program sv-benchmarks/c/recursive-simple/fibo_7_true-unreach-call_true-termination.c, a0bda9feccee812a2487069f4926cbe4decff2dbd38de0499ea31f5e0c23c28d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/a0bda9feccee812a2487069f4926cbe4decff2dbd38de0499ea31f5e0c23c28d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
15fcab4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 9 | 2017-11-30T14:42:13+01:00 | ||
0cebb04 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 5 | 2017-11-30T11:37:45+01:00 | ||
8d61051 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 6 | 2017-12-02T01:39:22+01:00 | ||
fcdd2e8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | VIAP | 50 | 2017-12-03T03:46 CET (sv-comp) | ||
dd3649d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 8 | 2017-12-03T01:30Z | ||
74a5950 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-01T23:53 CET (sv-comp) | ||
8962fd1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Map2Check | 4 | 2017-12-01T21:48 CET (sv-comp) | ||
31dbdf8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T01:50:08.181756 | ||
340db03 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T15:40:03.866061 | ||
e150b8a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T23:53:23.262584 | ||
15178f3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T08:41:10.690958 | ||
2cee8fb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 5 | 2017-12-01T16:33 CET (sv-comp) | ||
4bc2ca0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.12-svcomp17 | 4 | 2017-11-02T13:16:17+05:30 | ||
73e4e92 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 7 | 2017-11-30T20:41:23+01:00 | ||
3767715 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-03T06:51:06+01:00 | 43c9ead | |
a47e4ad | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-03T04:23:10+01:00 | 26628e9 | |
6ce3947 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-03T04:21:54+01:00 | 0e78f92 | |
e353221 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-03T01:39:07+01:00 | a975501 | |
b2aa410 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-02T20:34:03+01:00 | 7d82946 | |
e5b23bc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-02T09:00:27+01:00 | e3c5996 | |
760d634 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-01T22:37:51+01:00 | 7c93274 | |
3e12b13 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-01T22:04:49+01:00 | 5c69559 | |
89d865e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-01T08:13:06+01:00 | 6e2b26a | |
08483e3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-01T06:34:10+01:00 | 85da8d2 | |
d6a4d66 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-01T06:19:28+01:00 | cce381f | |
a1fa0fa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-11-30T14:40:45+01:00 | ||
58d3105 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 28 | 2017-11-30T21:38 CET (sv-comp) | ||
7cbddba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 8 | 2017-12-02T12:24Z | ||
fcf59cd | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 28 | 2017-12-01T19:13 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/fibo_7_true-unreach-call_true-termination.c, a0bda9feccee812a2487069f4926cbe4decff2dbd38de0499ea31f5e0c23c28d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/a0bda9feccee812a2487069f4926cbe4decff2dbd38de0499ea31f5e0c23c28d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |