Witness Inspection
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).
View and Validate the Witness
Input Given to this Service about the Witness (URL Query)
Key |
Value |
programName |
sv-benchmarks/c/float-benchs/cos_polynomial_true-unreach-call_true-termination.c |
programSHA |
6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd |
witnessName |
results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.cos_polynomial_true-unreach-call_true-termination.c.files/witness.graphml |
witnessSHA |
d1d25dc637fbaf827f472072e7c911a8ff1e29b66d07d110e357b1422c8e4c78 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/d1d25dc637fbaf827f472072e7c911a8ff1e29b66d07d110e357b1422c8e4c78.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-01T21:13:03.548324 |
producer |
ESBMC 4.6.0 kind |
program-sha256 |
6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd |
programfile |
../../sv-benchmarks/c/float-benchs/cos_polynomial_true-unreach-call_true-termination.c |
programhash |
2507b56afd4c82d08388837f279920ee2254841f |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/d1d25dc637fbaf827f472072e7c911a8ff1e29b66d07d110e357b1422c8e4c78.graphml |
witness-sha256 |
d1d25dc637fbaf827f472072e7c911a8ff1e29b66d07d110e357b1422c8e4c78 |
witness-size |
3418 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd, sv-benchmarks/c/float-benchs/cos_polynomial_true-unreach-call_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/float-benchs/cos_polynomial_true-unreach-call_true-termination.c, 6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd, sv-benchmarks/c/float-benchs/cos_polynomial_true-unreach-call_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/float-benchs/cos_polynomial_true-unreach-call_true-termination.c, 6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd, sv-benchmarks/c/float-benchs/cos_polynomial_true-unreach-call_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/float-benchs/cos_polynomial_true-unreach-call_true-termination.c, 6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '21
Trying to find witnesses for program (6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd, sv-benchmarks/c/float-benchs/cos_polynomial_true-unreach-call_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/float-benchs/cos_polynomial_true-unreach-call_true-termination.c, 6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '20
Trying to find witnesses for program (6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd, sv-benchmarks/c/float-benchs/cos_polynomial_true-unreach-call_true-termination.c).
Found 12 witnesses for program sv-benchmarks/c/float-benchs/cos_polynomial_true-unreach-call_true-termination.c, 6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
bf066b3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
Pinaka |
3 |
2019-12-03T22:21 CET (comp) |
|
58fc24b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
8 |
2019-12-11T20:23:04+01:00 |
f9e199f |
37822f1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
8 |
2019-12-11T20:02:31+01:00 |
59cbb9f |
5716353 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
8 |
2019-12-08T00:36:26+01:00 |
9f2c68a |
eeef7f7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
8 |
2019-12-07T23:46:03+01:00 |
855fbfe |
b39f2c3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
8 |
2019-12-05T19:13:09+01:00 |
c837347 |
138b5d4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
8 |
2019-12-05T19:03:07+01:00 |
fcbe184 |
ffb2c35 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
8 |
2019-12-04T02:07:33+01:00 |
bf066b3 |
6b4a726 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
8 |
2019-11-30T16:39:18+01:00 |
7fa8aa5 |
7fa8aa5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / svcomp20 |
8 |
2019-11-30T12:57:40+01:00 |
|
9f2c68a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.8 |
8 |
2019-12-07T15:44:37+01:00 |
|
855fbfe |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
BRICK |
3 |
2019-12-07T21:37:49Z |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd, sv-benchmarks/c/float-benchs/cos_polynomial_true-unreach-call_true-termination.c).
Found 13 witnesses for program sv-benchmarks/c/float-benchs/cos_polynomial_true-unreach-call_true-termination.c, 6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
8c61e2c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
Pinaka |
3 |
2018-12-07T09:53 CET (sv-comp) |
|
a6b8d27 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7 |
8 |
2018-12-10T18:26:43+01:00 |
|
a9ccea1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
8 |
2018-12-07T14:47:24+01:00 |
|
7c42189 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-10T20:32:15+01:00 |
a6b8d27 |
8619a1b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-08T06:20:22+01:00 |
a9ccea1 |
b0910dd |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-08T03:04:02+01:00 |
32310a5 |
d24a597 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-07T16:52:49+01:00 |
8c61e2c |
d14de60 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-06T09:43:29+01:00 |
33e6d6b |
d982f04 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-06T09:00:49+01:00 |
6475e2b |
632908a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-06T08:35:17+01:00 |
e030bf3 |
c684a0d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-06T08:20:34+01:00 |
353f28a |
244ed6f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-06T07:36:21+01:00 |
e108f57 |
6475e2b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
8 |
2018-12-06T04:38:37+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd, sv-benchmarks/c/float-benchs/cos_polynomial_true-unreach-call_true-termination.c).
Found 12 witnesses for program sv-benchmarks/c/float-benchs/cos_polynomial_true-unreach-call_true-termination.c, 6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
e3882d6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26725 |
8 |
2017-12-01T03:16:36+01:00 |
|
02cc7b7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker (unknown version) |
9 |
2017-12-02T00:01:05+01:00 |
|
d1d25dc |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 kind |
3 |
2017-12-01T21:13:03.548324 |
|
46f4456 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 incr |
3 |
2017-12-01T19:52:12.925668 |
|
30f0bd4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.12-svcomp17 |
4 |
2017-11-02T13:16:17+05:30 |
|
89ecc2c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
9 |
2017-12-03T04:13:35+01:00 |
43ca46e |
7e7504b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
9 |
2017-12-02T08:31:46+01:00 |
3212a99 |
b0122c5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
9 |
2017-12-01T22:48:28+01:00 |
9a1c57f |
ee6e58e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
9 |
2017-12-01T06:35:07+01:00 |
08e5c99 |
e8dbe2f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
9 |
2017-12-01T05:07:47+01:00 |
f04330d |
567f625 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CBMC |
9 |
2017-11-30T13:00 CET (sv-comp) |
|
2a5cebc |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
2LS |
20 |
2017-11-30T16:17 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd, sv-benchmarks/c/float-benchs/cos_polynomial_true-unreach-call_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/float-benchs/cos_polynomial_true-unreach-call_true-termination.c, 6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/6781d85575972fa81a64ce58706ae6fbc716f19d10f5f1c34209f6579c0e56fd.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |