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/eca-rers2012/Problem06_label10_false-unreach-call.c |
programSHA |
f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0 |
witnessName |
results-verified/cbmc.2018-12-04_2248.logfiles/sv-comp19_prop-reachsafety.Problem06_label10_false-unreach-call.c.files/witness.graphml |
witnessSHA |
1d2b0c635e6510149188d18f562577c9c52c251372debcad996164b760504bcd |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/1d2b0c635e6510149188d18f562577c9c52c251372debcad996164b760504bcd.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-05T06:01 CET (sv-comp) |
producer |
CBMC |
programfile |
../../sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c |
programhash |
cc3fbbe0f1e300e01cc35d4183862d780b407ac5 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/1d2b0c635e6510149188d18f562577c9c52c251372debcad996164b760504bcd.graphml |
witness-sha256 |
1d2b0c635e6510149188d18f562577c9c52c251372debcad996164b760504bcd |
witness-size |
732428 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0, sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c, f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0.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 (f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0, sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c, f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0.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 (f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0, sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c, f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0.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 (f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0, sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c, f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0.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 (f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0, sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c).
Found 10 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c, f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
8436c9c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
2 |
2019-12-01 14:43:15 |
|
fbb19de |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Pinaka |
589 |
2019-12-04T00:15 CET (comp) |
|
5b87264 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
2067 |
2019-12-11T21:40:19+01:00 |
0d66b59 |
12509c7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
2066 |
2019-12-11T21:09:35+01:00 |
8436c9c |
c4efe82 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
2067 |
2019-12-11T20:54:34+01:00 |
e9c2b90 |
8a1bfe2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
2067 |
2019-12-11T20:44:39+01:00 |
8eee1c7 |
c5035be |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
2768 |
2019-12-04T02:58:26+01:00 |
fbb19de |
73d25b8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
2067 |
2019-12-03T08:01:32+01:00 |
3f467e7 |
3f467e7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
2106 |
2019-11-29T21:37:15+01:00 |
|
0d66b59 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
2094 |
2019-11-30T23:20:05+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0, sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c).
Found 11 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c, f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
898afc3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2018-12-08T11:13 CET (sv-comp) |
|
58f4f46 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Pinaka |
639 |
2018-12-07T06:37 CET (sv-comp) |
|
e5037ce |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
2106 |
2018-12-07T16:53:25+01:00 |
|
ce662f3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
2067 |
2018-12-09T18:22:01+01:00 |
4ed07c0 |
f4da48b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
2067 |
2018-12-08T08:42:54+01:00 |
e5037ce |
2e00bef |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
2066 |
2018-12-08T05:04:34+01:00 |
98f6d6a |
e8e99c5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
2768 |
2018-12-07T17:45:55+01:00 |
58f4f46 |
5c5ce5f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
2067 |
2018-12-06T10:09:48+01:00 |
75e0bc5 |
1963708 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
2067 |
2018-12-06T09:48:54+01:00 |
68efadd |
269f301 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
2770 |
2018-12-06T09:15:11+01:00 |
1d2b0c6 |
68efadd |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
2106 |
2018-12-06T04:51:56+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0, sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c).
Found 5 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c, f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
ae17af2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2017-12-02T08:13 CET (sv-comp) |
|
69b33f2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
5 |
2017-12-02T02:23:05.790027 |
|
52071b6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
5 |
2017-12-01T16:23:44.707837 |
|
ec49949 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
1166 |
2017-11-30T18:09:08+01:00 |
|
ded981c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
731 |
2017-11-30T11:52 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0, sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label10_false-unreach-call.c, f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f13d55fd7be1e2e567de2a9cbf227f1aa94fa23e9d328028d11ad016eecd96c0.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |