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_true-unreach-call_true-termination.c |
programSHA | 167795186a7875003dc59ff165eb6862dab4cdd2a38cd62831f70434262cd59e |
witnessName | results-validated/cpa-seq-validate-correctness-witnesses-utaipan.2018-12-09_2012.logfiles/sv-comp19_prop-reachsafety.fibo_2calls_2_true-unreach-call_true-termination.c.files/witness.graphml |
witnessSHA | 135485f8d580274829488a51f98cb70200e8c663939ccd33f5e2ecac818b2fb5 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-09T20:35:49+01:00 |
inputwitnesshash | a491831efd3f3ef128c77acd3db2cdd3124a0ed16be36239179c9a8f573a39ae |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 167795186a7875003dc59ff165eb6862dab4cdd2a38cd62831f70434262cd59e |
programfile | ../../sv-benchmarks/c/recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c |
programhash | 167795186a7875003dc59ff165eb6862dab4cdd2a38cd62831f70434262cd59e |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/135485f8d580274829488a51f98cb70200e8c663939ccd33f5e2ecac818b2fb5.graphml |
witness-sha256 | 135485f8d580274829488a51f98cb70200e8c663939ccd33f5e2ecac818b2fb5 |
witness-size | 9082 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, 167795186a7875003dc59ff165eb6862dab4cdd2a38cd62831f70434262cd59e).
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c, 167795186a7875003dc59ff165eb6862dab4cdd2a38cd62831f70434262cd59e
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/167795186a7875003dc59ff165eb6862dab4cdd2a38cd62831f70434262cd59e.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_true-unreach-call_true-termination.c, 167795186a7875003dc59ff165eb6862dab4cdd2a38cd62831f70434262cd59e
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/167795186a7875003dc59ff165eb6862dab4cdd2a38cd62831f70434262cd59e.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_true-unreach-call_true-termination.c, 167795186a7875003dc59ff165eb6862dab4cdd2a38cd62831f70434262cd59e
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/167795186a7875003dc59ff165eb6862dab4cdd2a38cd62831f70434262cd59e.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_true-unreach-call_true-termination.c, 167795186a7875003dc59ff165eb6862dab4cdd2a38cd62831f70434262cd59e
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/167795186a7875003dc59ff165eb6862dab4cdd2a38cd62831f70434262cd59e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 16 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c, 167795186a7875003dc59ff165eb6862dab4cdd2a38cd62831f70434262cd59e
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/167795186a7875003dc59ff165eb6862dab4cdd2a38cd62831f70434262cd59e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
24044d4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:43 CET (comp) | ||
24dc9b9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T20:22:14+01:00 | e3178ad | |
898413b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T20:17:38+01:00 | 01e02ba | |
cf9331e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T20:02:32+01:00 | 7c4cba6 | |
6e771de | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-08T00:53:24+01:00 | 1652963 | |
d1c08f4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-07T23:27:27+01:00 | 94a0b76 | |
bff3ff8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-07T19:47:16+01:00 | 67220fa | |
9640fc1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-06T01:54:42+01:00 | 5601375 | |
e145b0d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-05T19:13:10+01:00 | c2eb1e7 | |
524e15e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-04T02:07:48+01:00 | 24044d4 | |
8d92ab1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-11-30T19:01:11+01:00 | 5dab902 | |
4d4271d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-11-30T16:34:31+01:00 | 2e867fa | |
2e867fa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 9 | 2019-11-29T21:14:55+01:00 | ||
1652963 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8 | 9 | 2019-12-07T22:21:10+01:00 | ||
01e02ba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 9 | 2019-12-01T18:04:18+01:00 | ||
979f5a7 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:17 CET (comp) |
Found 22 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c, 167795186a7875003dc59ff165eb6862dab4cdd2a38cd62831f70434262cd59e
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/167795186a7875003dc59ff165eb6862dab4cdd2a38cd62831f70434262cd59e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8f0b4fe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T05:33 CET (sv-comp) | ||
f461c9d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T08:44:36 | ||
2d4005e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T09:00 CET (sv-comp) | ||
579fdf8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 9 | 2018-12-08T01:15:18+01:00 | ||
d8e3d7f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-10T20:00:38+01:00 | 2d2352b | |
14c9d00 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-10T10:30:37+01:00 | cc7aaa7 | |
41e02ee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-09T21:06:23+01:00 | c0393c8 | |
135485f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-09T20:35:49+01:00 | a491831 | |
68fcfec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-09T20:11:27+01:00 | 2135416 | |
52747e0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T23:22:36+01:00 | 8f0b4fe | |
df59053 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T21:32:19+01:00 | f461c9d | |
4e4f2fe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T07:17:35+01:00 | 579fdf8 | |
98f52ba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T03:41:22+01:00 | 258e7f3 | |
68d5604 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T02:30:01+01:00 | cc7aaa7 | |
7de293a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-07T17:18:53+01:00 | 4d8d090 | |
accf3ac | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-07T16:39:29+01:00 | 2d4005e | |
54d6413 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T09:28:16+01:00 | 93c6c9e | |
d9f5d4b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T08:45:25+01:00 | 4d593a9 | |
aa0342c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T08:29:19+01:00 | 2b36951 | |
4d593a9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-05T15:06:22+01:00 | ||
c5d939a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T01:12 CET (sv-comp) | ||
0e3b915 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T04:40 CET (sv-comp) |
Found 34 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c, 167795186a7875003dc59ff165eb6862dab4cdd2a38cd62831f70434262cd59e
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/167795186a7875003dc59ff165eb6862dab4cdd2a38cd62831f70434262cd59e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4d8d090 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T22:54 CET (sv-comp) | ||
c0393c8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | VIAP | 7 | 2017-12-03T03:51 CET (sv-comp) | ||
b645504 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 11 | 2017-12-02T19:06Z | ||
5d4dcaf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T09:43 CET (sv-comp) | ||
5e2ff47 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Map2Check | 4 | 2017-12-01T21:14 CET (sv-comp) | ||
1b828af | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T00:07:21.319353 | ||
39cee3a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T09:31:17.991981 | ||
2f6eb7e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T14:12:15.401562 | ||
5131986 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T18:22:27.439147 | ||
2f2b13b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 5 | 2017-12-01T18:38 CET (sv-comp) | ||
ff3e7b7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 9 | 2017-12-02T23:00:43+01:00 | ||
e9dbd6b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-01T02:41:24+01:00 | ||
91d9baf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-03T06:51:19+01:00 | 205d1f1 | |
b743427 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-03T04:21:56+01:00 | dd97a23 | |
64f36af | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-03T04:16:19+01:00 | c210d5e | |
ac83849 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-03T00:36:55+01:00 | d16cd8c | |
4252fe6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-02T20:03:57+01:00 | 4079cef | |
46267d9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-02T14:53:42+01:00 | 7a5fe76 | |
360eff2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-02T08:20:22+01:00 | d6c5df7 | |
9f8a0b7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-02T00:14:57+01:00 | dccf7d6 | |
b72a9c2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T22:21:54+01:00 | 50842f9 | |
97f0a61 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T22:17:15+01:00 | 6b96b6e | |
c931d4f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T08:13:30+01:00 | cc2a3fd | |
fbc022a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T06:59:25+01:00 | 7583b7e | |
d459388 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T06:32:29+01:00 | 6eab777 | |
754dbba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T06:15:38+01:00 | 8a84fc6 | |
bf14e82 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T06:13:50+01:00 | 6ac740e | |
0565ac4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T00:40:10+01:00 | ||
97136b9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 16 | 2017-11-30T12:30:21+01:00 | ||
51bceba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 9 | 2017-11-30T20:28:36+01:00 | ||
c85e82c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 7 | 2017-12-01T23:16:34+01:00 | ||
1a29ca3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 6 | 2017-11-30T13:36 CET (sv-comp) | ||
3aeca09 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 11 | 2017-12-02T07:29Z | ||
5d540ea | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 6 | 2017-12-01T17:31 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c, 167795186a7875003dc59ff165eb6862dab4cdd2a38cd62831f70434262cd59e
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/167795186a7875003dc59ff165eb6862dab4cdd2a38cd62831f70434262cd59e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |