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_2calls_4_true-unreach-call_true-termination.c |
programSHA | b68a4c0486dd697452780f7d236fcbecbdf72b64560b0950a11b207de4adede6 |
witnessName | results-verified/pesco.2018-12-06_1244.logfiles/sv-comp19_prop-reachsafety.fibo_2calls_4_true-unreach-call_true-termination.c.files/witness.graphml |
witnessSHA | 884090169a23da27d312ce49d461eb186405524cf8aa568a072e0ef3ae40b09e |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T01:13:18+01:00 |
producer | CPAchecker 1.7-svn b8d6131600+ |
program-sha256 | b68a4c0486dd697452780f7d236fcbecbdf72b64560b0950a11b207de4adede6 |
programfile | ../../sv-benchmarks/c/recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c |
programhash | b68a4c0486dd697452780f7d236fcbecbdf72b64560b0950a11b207de4adede6 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/884090169a23da27d312ce49d461eb186405524cf8aa568a072e0ef3ae40b09e.graphml |
witness-sha256 | 884090169a23da27d312ce49d461eb186405524cf8aa568a072e0ef3ae40b09e |
witness-size | 8985 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, b68a4c0486dd697452780f7d236fcbecbdf72b64560b0950a11b207de4adede6).
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c, b68a4c0486dd697452780f7d236fcbecbdf72b64560b0950a11b207de4adede6
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/b68a4c0486dd697452780f7d236fcbecbdf72b64560b0950a11b207de4adede6.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_2calls_4_true-unreach-call_true-termination.c, b68a4c0486dd697452780f7d236fcbecbdf72b64560b0950a11b207de4adede6
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/b68a4c0486dd697452780f7d236fcbecbdf72b64560b0950a11b207de4adede6.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_2calls_4_true-unreach-call_true-termination.c, b68a4c0486dd697452780f7d236fcbecbdf72b64560b0950a11b207de4adede6
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/b68a4c0486dd697452780f7d236fcbecbdf72b64560b0950a11b207de4adede6.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_2calls_4_true-unreach-call_true-termination.c, b68a4c0486dd697452780f7d236fcbecbdf72b64560b0950a11b207de4adede6
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/b68a4c0486dd697452780f7d236fcbecbdf72b64560b0950a11b207de4adede6.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_2calls_4_true-unreach-call_true-termination.c, b68a4c0486dd697452780f7d236fcbecbdf72b64560b0950a11b207de4adede6
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/b68a4c0486dd697452780f7d236fcbecbdf72b64560b0950a11b207de4adede6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
119ed27 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-04T01:15 CET (comp) | ||
f9c7d1d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T20:25:38+01:00 | 7491271 | |
3a4eb89 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T20:17:10+01:00 | cc722fc | |
e5f76a0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T20:02:23+01:00 | 2a5d88b | |
a97b895 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-08T00:36:17+01:00 | ae645a5 | |
714b825 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-07T23:44:47+01:00 | d4e9b5e | |
6ed9b72 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-07T19:47:41+01:00 | 005bf09 | |
2601585 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-06T02:10:32+01:00 | 6af9441 | |
7d5febd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-05T19:12:50+01:00 | dcb97d2 | |
a25fe87 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-04T02:07:34+01:00 | 119ed27 | |
3f3a98a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-11-30T19:44:59+01:00 | 8ed8c9b | |
8bb762d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-11-30T16:58:44+01:00 | ed93248 | |
ed93248 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 9 | 2019-11-30T12:54:12+01:00 | ||
cc722fc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 9 | 2019-12-01T16:47:51+01:00 | ||
86f6947 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:42 CET (comp) |
Found 21 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c, b68a4c0486dd697452780f7d236fcbecbdf72b64560b0950a11b207de4adede6
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/b68a4c0486dd697452780f7d236fcbecbdf72b64560b0950a11b207de4adede6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
61cdb9d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T11:00 CET (sv-comp) | ||
6ab70b2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T15:47:58 | ||
976815e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T04:04 CET (sv-comp) | ||
8840901 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 9 | 2018-12-08T01:13:18+01:00 | ||
fb615d9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-10T20:15:08+01:00 | 1a5e633 | |
c4d88fe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-10T10:31:26+01:00 | 2310176 | |
e7ea82b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-09T21:06:40+01:00 | a66b5cd | |
a5fd171 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-09T20:20:35+01:00 | 437bbc6 | |
f690112 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-09T20:02:50+01:00 | 556f7f1 | |
81ed751 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T23:13:56+01:00 | 61cdb9d | |
d42f88c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T21:31:32+01:00 | 6ab70b2 | |
eae389b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T05:48:03+01:00 | 8840901 | |
fda9bdf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T04:23:53+01:00 | f0dae0b | |
7aaa060 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T02:09:47+01:00 | 2310176 | |
94cfc40 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-07T16:37:58+01:00 | 976815e | |
890666d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T09:28:16+01:00 | 6f32134 | |
4e45ecb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T09:08:09+01:00 | c1b4fd9 | |
038ca51 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T08:10:33+01:00 | d74268e | |
c1b4fd9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T07:42:30+01:00 | ||
49d75ab | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T14:22 CET (sv-comp) | ||
ba9864a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T06:17 CET (sv-comp) |
Found 29 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c, b68a4c0486dd697452780f7d236fcbecbdf72b64560b0950a11b207de4adede6
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/b68a4c0486dd697452780f7d236fcbecbdf72b64560b0950a11b207de4adede6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ac7c01f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 16 | 2017-11-30T13:21:18+01:00 | ||
0bd4e7e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 8 | 2017-11-30T13:40:32+01:00 | ||
4bbab74 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 9 | 2017-12-01T19:28:10+01:00 | ||
a66b5cd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | VIAP | 14 | 2017-12-03T03:49 CET (sv-comp) | ||
0cfcdf5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 11 | 2017-12-03T00:22Z | ||
e884756 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T01:12 CET (sv-comp) | ||
421f034 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Map2Check | 5 | 2017-12-01T20:57 CET (sv-comp) | ||
f959a2e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T00:22:00.964579 | ||
bd45c07 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T09:04:56.437502 | ||
9494642 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T21:39:57.557499 | ||
c5f92a0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T09:23:03.546201 | ||
ee3d00b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 7 | 2017-12-01T16:00 CET (sv-comp) | ||
93c3e21 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.12-svcomp17 | 4 | 2017-11-02T13:16:17+05:30 | ||
3b8437f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 10 | 2017-11-30T16:56:00+01:00 | ||
9695edb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-03T06:50:44+01:00 | d4c5824 | |
52b7a16 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-03T04:24:20+01:00 | 0c4cf58 | |
6a0b2a9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-03T04:21:46+01:00 | 1f74003 | |
383f4cc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-02T23:22:04+01:00 | 426649b | |
245cea5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-02T20:48:46+01:00 | ab6b0de | |
a28f411 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-02T07:41:37+01:00 | dd2a78c | |
b626797 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T22:21:33+01:00 | 60b7ca5 | |
f2c4460 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T22:04:53+01:00 | 6d6a895 | |
07027b9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T08:13:56+01:00 | 3ad9d93 | |
15a5ceb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T05:28:18+01:00 | a86ace1 | |
76e33a1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T05:27:17+01:00 | f5f8b67 | |
1b6fdd4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T02:15:53+01:00 | ||
4a26f30 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 10 | 2017-12-01T03:06 CET (sv-comp) | ||
2b47a8a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 11 | 2017-12-02T07:36Z | ||
5244912 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 10 | 2017-12-01T13:41 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c, b68a4c0486dd697452780f7d236fcbecbdf72b64560b0950a11b207de4adede6
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/b68a4c0486dd697452780f7d236fcbecbdf72b64560b0950a11b207de4adede6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |