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/loops/eureka_05_true-unreach-call_true-termination.i |
programSHA | 3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac |
witnessName | results-validated/cpa-seq-validate-correctness-witnesses-skink.2018-12-07_1709.logfiles/sv-comp19_prop-reachsafety.eureka_05_true-unreach-call_true-termination.i.files/witness.graphml |
witnessSHA | fa309568e8a3c19ae616d9f4415e58d62191a4bb314cf4122f51e4f06b7adbbc |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-07T17:59:20+01:00 |
inputwitnesshash | 07417c1f3899a0d5a06af35ed50eecde5edd1f62f6019874454215395555f9c5 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac |
programfile | ../../sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i |
programhash | 3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/fa309568e8a3c19ae616d9f4415e58d62191a4bb314cf4122f51e4f06b7adbbc.graphml |
witness-sha256 | fa309568e8a3c19ae616d9f4415e58d62191a4bb314cf4122f51e4f06b7adbbc |
witness-size | 8947 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, 3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac).
Found 0 witnesses for program sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i, 3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i, 3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i, 3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i, 3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 16 witnesses for program sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i, 3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
05cc91f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:23 CET (comp) | ||
efc7aaa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T20:19:56+01:00 | 0052936 | |
ddf1cda | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T20:17:54+01:00 | d29fa52 | |
1fe358e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T20:13:40+01:00 | 7939dda | |
3a80ea6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T20:03:11+01:00 | fcb7807 | |
13acdc2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-08T00:36:17+01:00 | ec4d8d2 | |
8c59699 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-06T01:53:42+01:00 | 320c40c | |
c253a47 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-05T19:13:01+01:00 | f8cdd36 | |
d3379fe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-05T19:03:03+01:00 | 0655583 | |
122debc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-04T02:07:31+01:00 | 05cc91f | |
82aaaf4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-11-30T19:37:32+01:00 | 277d681 | |
4b8e749 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-11-30T16:17:35+01:00 | b93e60b | |
b93e60b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 10 | 2019-11-30T00:26:32+01:00 | ||
ec4d8d2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8 | 10 | 2019-12-07T19:58:28+01:00 | ||
7939dda | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 10 | 2019-11-30T23:43:31+01:00 | ||
46260d8 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:01 CET (comp) |
Found 22 witnesses for program sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i, 3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c3a3cde | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T01:36 CET (sv-comp) | ||
3c1b532 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T07:28:34 | ||
c30f73f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T07:45 CET (sv-comp) | ||
fe4b6b9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7 | 10 | 2018-12-10T18:34:21+01:00 | ||
23d0ed1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 10 | 2018-12-07T03:37:49+01:00 | ||
cd78482 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-10T20:20:39+01:00 | fe4b6b9 | |
a771e92 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-10T10:45:22+01:00 | d956ccc | |
3ee8ffc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-09T21:21:17+01:00 | f1efd01 | |
70b14c1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-09T20:05:41+01:00 | 230edf3 | |
f69dbf4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T23:25:11+01:00 | c3a3cde | |
18e8399 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T21:46:56+01:00 | 3c1b532 | |
cfd5136 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T05:29:24+01:00 | 23d0ed1 | |
c9217db | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T03:34:45+01:00 | 033e4e9 | |
7ee6ec4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T02:19:01+01:00 | d956ccc | |
fa30956 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-07T17:59:20+01:00 | 07417c1 | |
b692186 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-07T16:53:45+01:00 | c30f73f | |
a41c9d7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T09:43:02+01:00 | dbffced | |
c988e7a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T09:07:45+01:00 | 7106966 | |
a6695dd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T07:40:52+01:00 | 0eca536 | |
7106966 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T06:53:45+01:00 | ||
91f6999 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T05:02 CET (sv-comp) | ||
1227a02 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T08:19 CET (sv-comp) |
Found 36 witnesses for program sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i, 3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
07417c1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T23:34 CET (sv-comp) | ||
f312912 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 9 | 2017-12-03T04:17Z | ||
9982fdc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T00:26 CET (sv-comp) | ||
e8cfb87 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Map2Check | 4 | 2017-12-01T21:27 CET (sv-comp) | ||
2c0e380 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 16 | 2017-12-02T20:16Z | ||
ef298c7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T01:22:27.019807 | ||
9b0d9bc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T09:29:06.729938 | ||
73a8920 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T00:07:50.593942 | ||
db0f1b0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T07:51:23.973832 | ||
ea98310 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 12 | 2017-12-01T19:47 CET (sv-comp) | ||
c9cb66c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 14 | 2017-12-02T19:17:29+01:00 | ||
25c105d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-01T00:23:11+01:00 | ||
35c4526 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-03T07:16:56+01:00 | 4e7d314 | |
17f7bef | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-03T04:27:21+01:00 | 1d0888f | |
db62643 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-03T02:53:39+01:00 | 7d2b8c8 | |
7ed4b5f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-03T02:00:26+01:00 | 0f380d5 | |
86e18c2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-02T20:38:50+01:00 | 5ec6e43 | |
c91d858 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-02T15:37:21+01:00 | de49114 | |
ffe924e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-02T08:20:38+01:00 | ac34d84 | |
28fc665 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-02T00:22:12+01:00 | 400bd1e | |
c41acce | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T22:40:54+01:00 | a1ccd83 | |
5170e0c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T22:31:55+01:00 | 3c6da8f | |
752511c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T08:27:32+01:00 | 0f8b1a0 | |
709f087 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T07:06:07+01:00 | 05a8590 | |
e670ca4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T05:43:37+01:00 | ae1c5ba | |
23ce00b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T05:41:17+01:00 | c1db767 | |
4663299 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 9 | 2017-12-01T05:31:58+01:00 | 7fc6d40 | |
9e9aa09 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 10 | 2017-12-01T02:39:01+01:00 | ||
91d53b8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 11 | 2017-11-30T11:45:31+01:00 | ||
bb843a9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 10 | 2017-11-30T18:21:13+01:00 | ||
d490425 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 9 | 2017-12-01T22:40:53+01:00 | ||
d5057a4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 31 | 2017-11-30T13:08 CET (sv-comp) | ||
dec3eb4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 9 | 2017-12-02T10:54Z | ||
009cfe8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 98 | 2017-11-30T20:37 CET (sv-comp) | ||
04778d6 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 30 | 2017-12-01T15:19 CET (sv-comp) | ||
a8b321c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 16 | 2017-12-01T11:54 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i, 3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |