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/floats-esbmc-regression/digits_while_true-unreach-call.i |
programSHA |
f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38 |
witnessName |
results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.digits_while_true-unreach-call.i.files/witness.graphml |
witnessSHA |
87b501e738b0bed1f910202898ad353d4f7ae24da0675dc0c8eea63f9881575b |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/87b501e738b0bed1f910202898ad353d4f7ae24da0675dc0c8eea63f9881575b.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-01T21:41:23.043608 |
producer |
ESBMC 4.6.0 kind |
program-sha256 |
f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38 |
programfile |
../../sv-benchmarks/c/floats-esbmc-regression/digits_while_true-unreach-call.i |
programhash |
ba87e9c753f7544044408266a9031a50ca559d39 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/87b501e738b0bed1f910202898ad353d4f7ae24da0675dc0c8eea63f9881575b.graphml |
witness-sha256 |
87b501e738b0bed1f910202898ad353d4f7ae24da0675dc0c8eea63f9881575b |
witness-size |
3410 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38, sv-benchmarks/c/floats-esbmc-regression/digits_while_true-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/floats-esbmc-regression/digits_while_true-unreach-call.i, f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38.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 (f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38, sv-benchmarks/c/floats-esbmc-regression/digits_while_true-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/floats-esbmc-regression/digits_while_true-unreach-call.i, f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38.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 (f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38, sv-benchmarks/c/floats-esbmc-regression/digits_while_true-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/floats-esbmc-regression/digits_while_true-unreach-call.i, f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38.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 (f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38, sv-benchmarks/c/floats-esbmc-regression/digits_while_true-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/floats-esbmc-regression/digits_while_true-unreach-call.i, f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38.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 (f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38, sv-benchmarks/c/floats-esbmc-regression/digits_while_true-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/floats-esbmc-regression/digits_while_true-unreach-call.i, f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38.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 '19
Trying to find witnesses for program (f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38, sv-benchmarks/c/floats-esbmc-regression/digits_while_true-unreach-call.i).
Found 15 witnesses for program sv-benchmarks/c/floats-esbmc-regression/digits_while_true-unreach-call.i, f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
a97d562 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
Symbiotic |
1 |
2018-12-08T07:17 CET (sv-comp) |
|
6eaf6e0 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
SMACK 1.9.3 |
3 |
2018-12-08T06:15:35 |
|
ced0656 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
Pinaka |
3 |
2018-12-06T23:58 CET (sv-comp) |
|
ab4d91e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-10T20:16:51+01:00 |
4f82619 |
22e4592 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-10T10:45:37+01:00 |
eda313b |
21a7ba9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-08T23:34:30+01:00 |
a97d562 |
26be119 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-08T21:49:55+01:00 |
6eaf6e0 |
424b724 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-08T04:43:43+01:00 |
d58fb9b |
3243d92 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-08T03:20:48+01:00 |
eda313b |
bd65bd7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-07T16:53:45+01:00 |
ced0656 |
e21fa16 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-06T09:10:06+01:00 |
2ecface |
607b009 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-06T08:24:57+01:00 |
f510c7c |
38ed3c8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-06T08:11:53+01:00 |
0ced02c |
57c7aad |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
5 |
2018-12-06T07:41:02+01:00 |
e8413c6 |
2ecface |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
142 |
2018-12-05T17:31:30+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38, sv-benchmarks/c/floats-esbmc-regression/digits_while_true-unreach-call.i).
Found 7 witnesses for program sv-benchmarks/c/floats-esbmc-regression/digits_while_true-unreach-call.i, f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
91b60b3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
35 |
2017-11-30T23:08 CET (sv-comp) |
|
b76cacd |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
Symbiotic |
1 |
2017-12-02T07:20 CET (sv-comp) |
|
87b501e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 kind |
3 |
2017-12-01T21:41:23.043608 |
|
04c759e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 incr |
3 |
2017-12-01T15:11:23.575762 |
|
9e8bf9f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.12-svcomp17 |
4 |
2017-11-02T13:16:17+05:30 |
|
66d0ce4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CBMC |
60 |
2017-11-30T13:50 CET (sv-comp) |
|
a808672 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
2LS |
83 |
2017-11-30T14:49 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38, sv-benchmarks/c/floats-esbmc-regression/digits_while_true-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/floats-esbmc-regression/digits_while_true-unreach-call.i, f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f1852a0446f6fcd785adc58f890b2e2b82ea83d7266b0ce4d62cc2a556e44f38.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |