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_label36_true-unreach-call_false-termination.c |
programSHA |
55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa |
witnessName |
results-verified/2ls.2017-12-01_1141.logfiles/sv-comp18.Problem14_label36_true-unreach-call_false-termination.c.files/witness.graphml |
witnessSHA |
a5b189d71060aea6ca1a018df304259bbc07056a4fb0696e8d6fa7ae5f679ee7 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/a5b189d71060aea6ca1a018df304259bbc07056a4fb0696e8d6fa7ae5f679ee7.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-01T16:31 CET (sv-comp) |
producer |
2LS |
program-sha256 |
55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa |
programfile |
../../sv-benchmarks/c/eca-rers2012/Problem14_label36_true-unreach-call_false-termination.c |
programhash |
16796b54e5e5e595ebddd1a211fd081adf88fc5e |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(F end) ) |
witness-file |
witnessFileByHash/a5b189d71060aea6ca1a018df304259bbc07056a4fb0696e8d6fa7ae5f679ee7.graphml |
witness-sha256 |
a5b189d71060aea6ca1a018df304259bbc07056a4fb0696e8d6fa7ae5f679ee7 |
witness-size |
575292 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa, sv-benchmarks/c/eca-rers2012/Problem14_label36_true-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label36_true-unreach-call_false-termination.c, 55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa.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 (55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa, sv-benchmarks/c/eca-rers2012/Problem14_label36_true-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label36_true-unreach-call_false-termination.c, 55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa.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 (55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa, sv-benchmarks/c/eca-rers2012/Problem14_label36_true-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label36_true-unreach-call_false-termination.c, 55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa.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 (55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa, sv-benchmarks/c/eca-rers2012/Problem14_label36_true-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label36_true-unreach-call_false-termination.c, 55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa.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 (55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa, sv-benchmarks/c/eca-rers2012/Problem14_label36_true-unreach-call_false-termination.c).
Found 9 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label36_true-unreach-call_false-termination.c, 55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
3b6fedc |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
301 |
2019-12-11T20:10:08+01:00 |
c5dae03 |
7ef8470 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
301 |
2019-12-11T20:03:02+01:00 |
b0649bf |
5abc6c0 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
301 |
2019-12-08T00:54:29+01:00 |
c8c8761 |
02aa17d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
301 |
2019-12-07T19:43:54+01:00 |
d9dd465 |
09ce4d2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
301 |
2019-12-05T19:02:56+01:00 |
b149e98 |
851182f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
301 |
2019-11-30T17:03:23+01:00 |
10aeee8 |
10aeee8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / svcomp20 |
307 |
2019-11-30T07:40:52+01:00 |
|
c5dae03 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
304 |
2019-12-01T05:37:52+01:00 |
|
e36551c |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
Symbiotic |
4 |
2019-12-01 08:38:12 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa, sv-benchmarks/c/eca-rers2012/Problem14_label36_true-unreach-call_false-termination.c).
Found 11 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label36_true-unreach-call_false-termination.c, 55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
88a375c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
308 |
2018-12-08T02:19:47+01:00 |
|
13034f7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-10T20:11:23+01:00 |
82779e8 |
bd46f9b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-09T20:22:51+01:00 |
fc5ede2 |
5e3cc3c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-09T20:03:17+01:00 |
10daefb |
11d6c85 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-09T19:48:56+01:00 |
956e8f1 |
4d3e4d1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-08T07:11:50+01:00 |
88a375c |
d3b0484 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-08T02:36:38+01:00 |
fe3b517 |
6c1d48b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-06T09:28:31+01:00 |
f8ba57a |
24de413 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-06T08:59:51+01:00 |
8f23f98 |
dd0a6f7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-06T07:59:55+01:00 |
de270da |
8f23f98 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
308 |
2018-12-05T17:33:07+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa, sv-benchmarks/c/eca-rers2012/Problem14_label36_true-unreach-call_false-termination.c).
Found 12 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label36_true-unreach-call_false-termination.c, 55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
6557ff9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.12-svcomp17 |
4 |
2017-11-02T13:16:17+05:30 |
|
d367cb6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
301 |
2017-12-03T04:05:38+01:00 |
fabe1ab |
18d24cf |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
301 |
2017-12-03T01:54:04+01:00 |
1745f16 |
53f20d1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
301 |
2017-12-01T06:30:31+01:00 |
6cf830c |
0ee15c0 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
301 |
2017-12-01T05:53:25+01:00 |
c280fd4 |
acd1868 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
301 |
2017-12-01T04:29:59+01:00 |
0a71c20 |
3bb58f4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
300 |
2017-11-30T23:06:43+01:00 |
|
0005c4f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26725 |
300 |
2017-11-30T21:46:44+01:00 |
|
33b93e3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
Automizer |
210 |
2017-12-02T16:03Z |
|
e0f18ba |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
2LS |
997 |
2017-11-30T16:29 CET (sv-comp) |
|
6e3f496 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
Automizer |
147 |
2017-12-03T11:17Z |
|
a5b189d |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
2LS |
575 |
2017-12-01T16:31 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa, sv-benchmarks/c/eca-rers2012/Problem14_label36_true-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label36_true-unreach-call_false-termination.c, 55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/55a15744a96d4c017cfd913c19437b10efcdfeeb08853e54d7f75b3ea2d566aa.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |