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/Problem03_label45_false-unreach-call.c |
programSHA |
dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8 |
witnessName |
results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.Problem03_label45_false-unreach-call.c.files/witness.graphml |
witnessSHA |
b3cab649e60e47acb26801902e9698d8b2962b5fd4ed18fece00d51826a2aab4 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/b3cab649e60e47acb26801902e9698d8b2962b5fd4ed18fece00d51826a2aab4.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-02T01:27:02.511223 |
producer |
ESBMC 4.6.0 kind |
program-sha256 |
dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8 |
programfile |
../../sv-benchmarks/c/eca-rers2012/Problem03_label45_false-unreach-call.c |
programhash |
2d61e70dd0544c9d7e5a2b57a59308fce8956039 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/b3cab649e60e47acb26801902e9698d8b2962b5fd4ed18fece00d51826a2aab4.graphml |
witness-sha256 |
b3cab649e60e47acb26801902e9698d8b2962b5fd4ed18fece00d51826a2aab4 |
witness-size |
4793 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8, sv-benchmarks/c/eca-rers2012/Problem03_label45_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label45_false-unreach-call.c, dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8.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 (dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8, sv-benchmarks/c/eca-rers2012/Problem03_label45_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label45_false-unreach-call.c, dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8.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 (dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8, sv-benchmarks/c/eca-rers2012/Problem03_label45_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label45_false-unreach-call.c, dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8.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 (dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8, sv-benchmarks/c/eca-rers2012/Problem03_label45_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label45_false-unreach-call.c, dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8.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 (dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8, sv-benchmarks/c/eca-rers2012/Problem03_label45_false-unreach-call.c).
Found 12 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label45_false-unreach-call.c, dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
cbf859c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
2 |
2019-12-02 00:38:47 |
|
5c7be87 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Pinaka |
164 |
2019-12-04T00:27 CET (comp) |
|
456488f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
561 |
2019-12-11T21:40:51+01:00 |
6aefcf9 |
f2da470 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
561 |
2019-12-11T21:09:20+01:00 |
cbf859c |
c32d0c2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
561 |
2019-12-11T20:55:25+01:00 |
7e108a3 |
1405512 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
561 |
2019-12-11T20:44:37+01:00 |
5b78c07 |
415e292 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
564 |
2019-12-08T01:51:53+01:00 |
362bbc4 |
db849a1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
751 |
2019-12-04T02:58:24+01:00 |
5c7be87 |
4b1a7bf |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
561 |
2019-12-03T08:09:03+01:00 |
c5273f8 |
c5273f8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
562 |
2019-11-30T08:22:34+01:00 |
|
6aefcf9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
562 |
2019-12-01T19:01:48+01:00 |
|
0b8806c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
685 |
2019-12-08T00:27:10+01:00 |
e488e7c |
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8, sv-benchmarks/c/eca-rers2012/Problem03_label45_false-unreach-call.c).
Found 15 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label45_false-unreach-call.c, dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
511a87e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2018-12-08T04:42 CET (sv-comp) |
|
3ad90dd |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
13 |
2018-12-08T09:19:49 |
|
110682f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
567 |
2018-12-06T20:36:55+01:00 |
|
629ef5a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
564 |
2018-12-10T20:35:06+01:00 |
da641bd |
b2c31cf |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
561 |
2018-12-09T18:20:04+01:00 |
5e3f325 |
5c168c7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
566 |
2018-12-08T23:43:37+01:00 |
511a87e |
1142b88 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
561 |
2018-12-08T22:08:44+01:00 |
3ad90dd |
28d3e1a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
561 |
2018-12-08T08:04:14+01:00 |
110682f |
e106e35 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
561 |
2018-12-08T05:05:06+01:00 |
f14b40a |
9c39948 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
561 |
2018-12-06T10:14:22+01:00 |
f9fd3be |
263627e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
561 |
2018-12-06T09:48:31+01:00 |
ae06a22 |
cb2032a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
752 |
2018-12-06T09:16:15+01:00 |
91d6756 |
ae06a22 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
562 |
2018-12-05T15:55:19+01:00 |
|
0849f37 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
685 |
2018-12-09T20:54:28+01:00 |
e4445b6 |
7d146d7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
685 |
2018-12-09T20:34:41+01:00 |
65d7f68 |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8, sv-benchmarks/c/eca-rers2012/Problem03_label45_false-unreach-call.c).
Found 9 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label45_false-unreach-call.c, dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
b51a3eb |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Veriabs |
3 |
2017-12-03T03:37 CET (sv-comp) |
|
b3cab64 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
5 |
2017-12-02T01:27:02.511223 |
|
620d170 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
5 |
2017-12-01T15:56:11.964046 |
|
9e87603 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
21 |
2017-12-01T04:04 CET (sv-comp) |
|
74f1b11 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
321 |
2017-11-30T19:50:00+01:00 |
|
00d81ae |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26758M |
1264 |
2017-11-30T12:37:38+01:00 |
|
edd22e2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26725 |
315 |
2017-12-01T01:08:28+01:00 |
|
0c5b7d1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
202 |
2017-12-01T00:50 CET (sv-comp) |
|
efdd1eb |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
2LS |
203 |
2017-12-01T03:18 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8, sv-benchmarks/c/eca-rers2012/Problem03_label45_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label45_false-unreach-call.c, dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/dada586dba950d5e0a31ece15d5b9f4528eced27ffae3768bf363bf6771796c8.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |