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/id_i10_o10_true-unreach-call_true-termination.c |
programSHA | c1fd3384e2df1362e5e0642f74f85aac6ed41dffb220917aa5659f5314429b9d |
witnessName | results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.id_i10_o10_true-unreach-call_true-termination.c.files/witness.graphml |
witnessSHA | 6261e3f4fc9eb0364d2917d8c94b5be6dddc7ffed8b00a9ad438c4c52d0314b6 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-02T05:19:35.101715 |
producer | ESBMC 4.6.0 kind |
program-sha256 | c1fd3384e2df1362e5e0642f74f85aac6ed41dffb220917aa5659f5314429b9d |
programfile | ../../sv-benchmarks/c/recursive-simple/id_i10_o10_true-unreach-call_true-termination.c |
programhash | d354f5dc1a4e4616bf2c7c7fc4888805a134a8dd |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/6261e3f4fc9eb0364d2917d8c94b5be6dddc7ffed8b00a9ad438c4c52d0314b6.graphml |
witness-sha256 | 6261e3f4fc9eb0364d2917d8c94b5be6dddc7ffed8b00a9ad438c4c52d0314b6 |
witness-size | 3418 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_i10_o10_true-unreach-call_true-termination.c, c1fd3384e2df1362e5e0642f74f85aac6ed41dffb220917aa5659f5314429b9d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/c1fd3384e2df1362e5e0642f74f85aac6ed41dffb220917aa5659f5314429b9d.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/id_i10_o10_true-unreach-call_true-termination.c, c1fd3384e2df1362e5e0642f74f85aac6ed41dffb220917aa5659f5314429b9d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/c1fd3384e2df1362e5e0642f74f85aac6ed41dffb220917aa5659f5314429b9d.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/id_i10_o10_true-unreach-call_true-termination.c, c1fd3384e2df1362e5e0642f74f85aac6ed41dffb220917aa5659f5314429b9d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/c1fd3384e2df1362e5e0642f74f85aac6ed41dffb220917aa5659f5314429b9d.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/id_i10_o10_true-unreach-call_true-termination.c, c1fd3384e2df1362e5e0642f74f85aac6ed41dffb220917aa5659f5314429b9d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/c1fd3384e2df1362e5e0642f74f85aac6ed41dffb220917aa5659f5314429b9d.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/id_i10_o10_true-unreach-call_true-termination.c, c1fd3384e2df1362e5e0642f74f85aac6ed41dffb220917aa5659f5314429b9d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/c1fd3384e2df1362e5e0642f74f85aac6ed41dffb220917aa5659f5314429b9d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c35d078 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:55 CET (comp) | ||
2e55b5b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-11T20:29:49+01:00 | 19f3331 | |
ee80811 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-11T20:21:40+01:00 | bc73df9 | |
87a0af5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-11T20:16:12+01:00 | f347c21 | |
da7221d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-11T20:02:19+01:00 | 1c5e0ae | |
d7aa84f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-08T00:38:01+01:00 | 70c1362 | |
ad3c23a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-07T23:40:51+01:00 | faf5598 | |
d7500c0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-07T19:43:40+01:00 | aca82f1 | |
b030530 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-06T02:05:44+01:00 | 0635fea | |
55e8d94 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-05T19:19:34+01:00 | 9acf150 | |
149f275 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-04T02:07:47+01:00 | c35d078 | |
376c64e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-11-30T19:41:09+01:00 | 39f625a | |
ba96409 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-11-30T17:18:22+01:00 | d899fef | |
d899fef | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 5 | 2019-11-29T16:41:15+01:00 | ||
bc73df9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 5 | 2019-12-01T05:00:38+01:00 | ||
bb3dc45 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:51 CET (comp) |
Found 23 witnesses for program sv-benchmarks/c/recursive-simple/id_i10_o10_true-unreach-call_true-termination.c, c1fd3384e2df1362e5e0642f74f85aac6ed41dffb220917aa5659f5314429b9d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/c1fd3384e2df1362e5e0642f74f85aac6ed41dffb220917aa5659f5314429b9d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4eba83d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T14:42 CET (sv-comp) | ||
f164b5c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T12:06:44 | ||
33b7269 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T10:26 CET (sv-comp) | ||
ae3ea12 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 5 | 2018-12-07T10:30:24+01:00 | ||
e3e0344 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-10T19:38:23+01:00 | 3aa8409 | |
b0f8c28 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-10T10:31:01+01:00 | b78e970 | |
d6587a1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-09T21:06:21+01:00 | f470bbd | |
a8a1d08 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-09T20:26:40+01:00 | 83c45dd | |
94c3823 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-09T19:38:27+01:00 | 0d37de6 | |
53fafdd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-09T17:25:28+01:00 | 21dd189 | |
eb5a140 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T23:09:57+01:00 | 4eba83d | |
c6c94a4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T21:35:34+01:00 | f164b5c | |
d7fd4e2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T06:32:37+01:00 | ae3ea12 | |
e17cd6e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T04:18:28+01:00 | db12fed | |
f2c4dc7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T02:03:51+01:00 | b78e970 | |
07d089c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-07T17:45:22+01:00 | cf012fc | |
95cd81a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-07T16:39:26+01:00 | 33b7269 | |
d93ca5d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:28:18+01:00 | f27e088 | |
48da66e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:05:24+01:00 | 8688637 | |
cb89ea3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T08:25:27+01:00 | 401c5d9 | |
8688637 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-05T11:41:39+01:00 | ||
14b43dc | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T06:03 CET (sv-comp) | ||
90c4580 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T09:37 CET (sv-comp) |
Found 33 witnesses for program sv-benchmarks/c/recursive-simple/id_i10_o10_true-unreach-call_true-termination.c, c1fd3384e2df1362e5e0642f74f85aac6ed41dffb220917aa5659f5314429b9d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/c1fd3384e2df1362e5e0642f74f85aac6ed41dffb220917aa5659f5314429b9d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d1c587a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 9 | 2017-12-01T03:45:41+01:00 | ||
c61e3ad | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 5 | 2017-12-01T01:46:27+01:00 | ||
0840990 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 6 | 2017-12-02T10:18:18+01:00 | ||
cf012fc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T23:10 CET (sv-comp) | ||
f470bbd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | VIAP | 12 | 2017-12-03T03:44 CET (sv-comp) | ||
aaf6221 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 6 | 2017-12-03T02:39Z | ||
44b2892 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T00:27 CET (sv-comp) | ||
9286b15 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Map2Check | 3 | 2017-12-01T20:37 CET (sv-comp) | ||
3674bfa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 6 | 2017-12-02T04:47Z | ||
e00f829 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T21:01:43.237769 | ||
4ee1c37 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T14:40:04.921194 | ||
6261e3f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T05:19:35.101715 | ||
22fbabc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T19:43:09.068853 | ||
108be95 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 4 | 2017-12-01T18:15 CET (sv-comp) | ||
1fe7d30 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.12-svcomp17 | 4 | 2017-11-02T13:16:17+05:30 | ||
965b7f9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 6 | 2017-11-30T23:45:53+01:00 | ||
4032c95 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-03T06:50:42+01:00 | accca57 | |
235e130 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-03T04:23:05+01:00 | 2d1ac2b | |
3499bb1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-03T04:08:01+01:00 | fa25f07 | |
735bd34 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-03T02:32:38+01:00 | 2616591 | |
76f5379 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-03T00:09:51+01:00 | f15a87a | |
406f6fa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-02T20:25:04+01:00 | 4b4fae9 | |
b94a94f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-02T08:32:28+01:00 | 808379d | |
fdb22cd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-02T00:08:41+01:00 | f03ba68 | |
9d9166a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-01T22:37:41+01:00 | 7dff0da | |
91a724b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-01T22:04:45+01:00 | 4c90f6a | |
8daa5f8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-01T08:12:14+01:00 | dba895a | |
efb1361 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-01T06:46:38+01:00 | 23200f9 | |
4ecebbe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-01T04:50:27+01:00 | fff9dce | |
51971b6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-11-30T12:50:48+01:00 | ||
622bf5a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 10 | 2017-11-30T14:06 CET (sv-comp) | ||
89768e1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 6 | 2017-12-02T16:41Z | ||
acf767c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 10 | 2017-12-01T13:18 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_i10_o10_true-unreach-call_true-termination.c, c1fd3384e2df1362e5e0642f74f85aac6ed41dffb220917aa5659f5314429b9d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/c1fd3384e2df1362e5e0642f74f85aac6ed41dffb220917aa5659f5314429b9d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |