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_2_false-unreach-call_true-termination.c |
programSHA | 30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f |
witnessName | results-verified/esbmc-incr.2017-12-01_0849.logfiles/sv-comp18.fibo_2calls_2_false-unreach-call_true-termination.c.files/witness.graphml |
witnessSHA | e72b26a37003a57f3faae8bb3177be76cee069ac98d7829c24a3a493e8f2965e |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-01T09:22:52.221007 |
producer | ESBMC 4.6.0 incr |
program-sha256 | 30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f |
programfile | ../../sv-benchmarks/c/recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c |
programhash | 0d7907681604b1ce9d21af31806cc60e045b313d |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/e72b26a37003a57f3faae8bb3177be76cee069ac98d7829c24a3a493e8f2965e.graphml |
witness-sha256 | e72b26a37003a57f3faae8bb3177be76cee069ac98d7829c24a3a493e8f2965e |
witness-size | 3620 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c, 30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f.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_2_false-unreach-call_true-termination.c, 30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f.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_2_false-unreach-call_true-termination.c, 30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f.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_2_false-unreach-call_true-termination.c, 30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 18 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c, 30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
18377d7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-02 00:27:13 | ||
86f2b29 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 6 | 2019-12-03T23:33 CET (comp) | ||
95adc82 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T21:42:49+01:00 | 34ed61b | |
2a58904 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T21:39:10+01:00 | 6cb2ea9 | |
a90e39d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T21:09:17+01:00 | 18377d7 | |
f98ceaf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T20:54:21+01:00 | 18c63bd | |
06b257e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T20:44:44+01:00 | 6cd14c1 | |
638b101 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-08T00:27:00+01:00 | bd5ec78 | |
328ef21 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-07T21:16:47+01:00 | e71bf50 | |
46f464f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-06T02:38:03+01:00 | abc1a56 | |
c8ada11 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-04T02:58:17+01:00 | 86f2b29 | |
877fae7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-03T08:57:03+01:00 | 138a206 | |
7b65af8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-03T08:08:36+01:00 | a4600a5 | |
a4600a5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 8 | 2019-11-30T12:13:40+01:00 | ||
34ed61b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 8 | 2019-12-01T00:31:04+01:00 | ||
2b8442a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-08T01:51:17+01:00 | 0810c10 | |
fd79ab4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-05T20:20:22+01:00 | a6c40f2 | |
de9b522 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:25 CET (comp) |
Found 26 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c, 30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2c3e065 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T00:42 CET (sv-comp) | ||
558cd67 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 4 | 2018-12-08T03:44:40 | ||
4066930 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 7 | 2018-12-06T22:53 CET (sv-comp) | ||
65cee7d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 9 | 2018-12-08T00:39:08+01:00 | ||
497d369 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-10T10:48:41+01:00 | 9d5dc5d | |
b548f65 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-09T21:23:32+01:00 | e65c164 | |
34b10e3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-09T20:29:52+01:00 | 55e468b | |
bfc4f00 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-09T18:20:43+01:00 | 12e04a3 | |
c0b64b9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T23:43:39+01:00 | 2c3e065 | |
c6b1fce | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-08T22:11:14+01:00 | 558cd67 | |
a900738 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T08:57:30+01:00 | 65cee7d | |
683c069 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T05:03:15+01:00 | 6ef8b72 | |
ab23555 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T04:37:06+01:00 | 9d5dc5d | |
6652e86 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-07T18:47:49+01:00 | fd03b64 | |
7118027 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-07T17:43:00+01:00 | 4066930 | |
f605968 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-07T01:16:28+01:00 | 10e7d7f | |
33342ee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T10:14:21+01:00 | c8b2395 | |
614bd97 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T09:48:57+01:00 | 4a294a7 | |
4a294a7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-05T07:51:30+01:00 | ||
4625c30 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-10T20:37:51+01:00 | 6ced7f5 | |
8649a86 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-09T20:53:10+01:00 | acb9fc8 | |
9a81028 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-09T20:37:18+01:00 | c4e70fa | |
8176170 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T09:19:26+01:00 | 4417557 | |
2ee626d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T09:19:05+01:00 | 277a773 | |
f38cfbe | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T11:49 CET (sv-comp) | ||
3299cc4 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T03:52 CET (sv-comp) |
Found 20 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c, 30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6ac115e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | skink | 3 | 2017-12-01T22:36 CET (sv-comp) | ||
0c17191 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | VeriAbs 1.3 | 6 | Sat Dec 2 17:31:54 2017 | ||
e65c164 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | VIAP | 7 | 2017-12-03T04:01 CET (sv-comp) | ||
056be1f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 9 | 2017-12-03T05:06Z | ||
784c826 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T08:53 CET (sv-comp) | ||
6f593d9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Map2Check | 5 | 2017-12-01T21:44 CET (sv-comp) | ||
8c830b2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 9 | 2017-12-02T01:40Z | ||
1be896e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-01T19:31:13.120774 | ||
e72b26a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T09:22:52.221007 | ||
8a65a84 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 5 | 2017-12-01T18:58 CET (sv-comp) | ||
8c34101 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 5 | 2017-12-01T03:07 CET (sv-comp) | ||
171f84e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-11-30T17:46:28+01:00 | ||
63bea5b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 14 | 2017-12-01T00:10:47+01:00 | ||
7dff649 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 8 | 2017-11-30T19:17:29+01:00 | ||
38459e4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 8 | 2017-12-01T21:51:06+01:00 | ||
e2dc3b5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 6 | 2017-11-30T18:42 CET (sv-comp) | ||
957afce | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 9 | 2017-12-02T19:07Z | ||
6d76136 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T00:28:58.258544 | ||
6dfcee6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T08:26:56.082634 | ||
e367b64 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 5 | 2017-12-01T13:53 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c, 30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/30ff92ec27b562a9abf134734bed6d3c2409b253fa804d26faa750b75f73899f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |