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/Problem14_label54_false-unreach-call_false-termination.c |
programSHA |
2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195 |
witnessName |
results-verified/depthk.2017-12-01_1515.logfiles/sv-comp18.Problem14_label54_false-unreach-call_false-termination.c.files/witness.graphml |
witnessSHA |
2bbb1fbb903824a0a1f297f59251abc550a5526053cb7b8dc213cd8841619eb8 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/2bbb1fbb903824a0a1f297f59251abc550a5526053cb7b8dc213cd8841619eb8.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-01T19:04 CET (sv-comp) |
memoryModel |
precise |
producer |
ESBMC 3.1 |
program-sha256 |
2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_dc264fb5-661c-4148-a907-aab34809c7f0/sv-benchmarks/c/eca-rers2012/Problem14_label54_false-unreach-call_false-termination.c |
programhash |
e5f4f52c7ffc2180fa6be90ab22725a89620d9be |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/2bbb1fbb903824a0a1f297f59251abc550a5526053cb7b8dc213cd8841619eb8.graphml |
witness-sha256 |
2bbb1fbb903824a0a1f297f59251abc550a5526053cb7b8dc213cd8841619eb8 |
witness-size |
23086 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195, sv-benchmarks/c/eca-rers2012/Problem14_label54_false-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label54_false-unreach-call_false-termination.c, 2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195.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 (2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195, sv-benchmarks/c/eca-rers2012/Problem14_label54_false-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label54_false-unreach-call_false-termination.c, 2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195.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 (2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195, sv-benchmarks/c/eca-rers2012/Problem14_label54_false-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label54_false-unreach-call_false-termination.c, 2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195.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 (2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195, sv-benchmarks/c/eca-rers2012/Problem14_label54_false-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label54_false-unreach-call_false-termination.c, 2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195.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 (2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195, sv-benchmarks/c/eca-rers2012/Problem14_label54_false-unreach-call_false-termination.c).
Found 11 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label54_false-unreach-call_false-termination.c, 2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
1408dbf |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
4 |
2019-12-01 05:03:37 |
|
91ecc72 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Pinaka |
413 |
2019-12-04T00:16 CET (comp) |
|
e646e46 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
1333 |
2019-12-11T21:09:11+01:00 |
1408dbf |
a27525c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
1492 |
2019-12-11T20:44:43+01:00 |
105a8ba |
8b92daa |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
1666 |
2019-12-04T02:58:14+01:00 |
91ecc72 |
0a04413 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
1333 |
2019-12-03T08:08:34+01:00 |
c128a19 |
c128a19 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
1332 |
2019-11-29T15:31:47+01:00 |
|
807d344 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
301 |
2019-12-11T20:54:40+01:00 |
07767a1 |
cefe50e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
301 |
2019-12-07T21:19:38+01:00 |
ba14d5e |
7668442 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
301 |
2019-12-05T20:22:04+01:00 |
fb93485 |
0968cf5 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
Symbiotic |
4 |
2019-12-01 13:44:44 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195, sv-benchmarks/c/eca-rers2012/Problem14_label54_false-unreach-call_false-termination.c).
Found 15 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label54_false-unreach-call_false-termination.c, 2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
f3284a0 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2018-12-08T18:37 CET (sv-comp) |
|
0d9d7f8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Pinaka |
483 |
2018-12-06T23:53 CET (sv-comp) |
|
552b645 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
1337 |
2018-12-07T01:37:01+01:00 |
|
26c47cd |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
1333 |
2018-12-09T18:16:54+01:00 |
c281187 |
ee572a9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
1333 |
2018-12-08T08:23:52+01:00 |
552b645 |
c33ffa5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
1667 |
2018-12-07T17:44:47+01:00 |
0d9d7f8 |
e719fae |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
1333 |
2018-12-06T09:48:19+01:00 |
34d64b2 |
bb00272 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
1816 |
2018-12-06T09:19:59+01:00 |
1cf69ea |
34d64b2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
1333 |
2018-12-05T22:04:07+01:00 |
|
f8f0a98 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-10T20:36:21+01:00 |
8745a93 |
9fdd13b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-09T20:53:45+01:00 |
2887739 |
7b0377c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-09T20:39:45+01:00 |
285af8c |
74de2a7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-08T23:43:36+01:00 |
f3284a0 |
d8951f8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-08T05:04:37+01:00 |
b4a659a |
5a04357 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-06T10:12:21+01:00 |
354fd77 |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195, sv-benchmarks/c/eca-rers2012/Problem14_label54_false-unreach-call_false-termination.c).
Found 13 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label54_false-unreach-call_false-termination.c, 2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
ed268b9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
VeriAbs 1.3 |
736 |
Sat Dec 2 19:21:13 2017 |
|
ec398a8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2017-12-02T04:00 CET (sv-comp) |
|
bc79a7b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
8 |
2017-12-01T13:17:57.682134 |
|
df363d3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
9 |
2017-12-01T11:47:25.148305 |
|
2bbb1fb |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
23 |
2017-12-01T19:04 CET (sv-comp) |
|
48e8bfa |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
717 |
2017-12-01T00:48:38+01:00 |
|
0e2c32f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26758M |
966 |
2017-11-30T20:53:29+01:00 |
|
dbec889 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26725 |
715 |
2017-12-01T00:02:49+01:00 |
|
9ab7a3a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
584 |
2017-11-30T12:52 CET (sv-comp) |
|
e7d79ec |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Automizer |
1019 |
2017-12-02T13:57Z |
|
e7f4d95 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
2LS |
547 |
2017-11-30T23:48 CET (sv-comp) |
|
0de9629 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
Automizer |
147 |
2017-12-03T11:15Z |
|
fa3146b |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
2LS |
577 |
2017-12-01T13:46 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195, sv-benchmarks/c/eca-rers2012/Problem14_label54_false-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label54_false-unreach-call_false-termination.c, 2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/2bad0b776d4394249cd61ba394cf3084621852d2a6f2a5bb023bc6bc3251a195.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |