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_label14_false-unreach-call_false-termination.c |
programSHA |
738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62 |
witnessName |
results-verified/2ls.2017-12-01_1141.logfiles/sv-comp18.Problem14_label14_false-unreach-call_false-termination.c.files/witness.graphml |
witnessSHA |
037eea0f6ca5571af3bc85b2fcea243059049effbdf38078b5560e39cdbe71f0 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/037eea0f6ca5571af3bc85b2fcea243059049effbdf38078b5560e39cdbe71f0.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-01T15:07 CET (sv-comp) |
producer |
2LS |
program-sha256 |
738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62 |
programfile |
../../sv-benchmarks/c/eca-rers2012/Problem14_label14_false-unreach-call_false-termination.c |
programhash |
a8b7062793a4a956381b28b9ce3638daa166e644 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(F end) ) |
witness-file |
witnessFileByHash/037eea0f6ca5571af3bc85b2fcea243059049effbdf38078b5560e39cdbe71f0.graphml |
witness-sha256 |
037eea0f6ca5571af3bc85b2fcea243059049effbdf38078b5560e39cdbe71f0 |
witness-size |
577274 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62, sv-benchmarks/c/eca-rers2012/Problem14_label14_false-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label14_false-unreach-call_false-termination.c, 738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62.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 (738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62, sv-benchmarks/c/eca-rers2012/Problem14_label14_false-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label14_false-unreach-call_false-termination.c, 738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62.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 (738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62, sv-benchmarks/c/eca-rers2012/Problem14_label14_false-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label14_false-unreach-call_false-termination.c, 738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62.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 (738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62, sv-benchmarks/c/eca-rers2012/Problem14_label14_false-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label14_false-unreach-call_false-termination.c, 738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62.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 (738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62, sv-benchmarks/c/eca-rers2012/Problem14_label14_false-unreach-call_false-termination.c).
Found 12 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label14_false-unreach-call_false-termination.c, 738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
a4ad2a2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
3 |
2019-12-01 13:16:42 |
|
2c79d34 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Pinaka |
311 |
2019-12-04T00:13 CET (comp) |
|
be5e867 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
986 |
2019-12-11T21:09:35+01:00 |
a4ad2a2 |
1e97039 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
986 |
2019-12-11T20:44:49+01:00 |
e12619f |
30b6f1e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
1212 |
2019-12-04T02:58:08+01:00 |
2c79d34 |
7b2dd0f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
986 |
2019-12-03T08:10:44+01:00 |
9d2cda4 |
9d2cda4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
986 |
2019-11-30T03:08:38+01:00 |
|
0ff8028 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
301 |
2019-12-11T20:55:03+01:00 |
0609b00 |
f3404eb |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
301 |
2019-12-07T21:19:28+01:00 |
61a95c4 |
76c1036 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
301 |
2019-12-05T20:21:37+01:00 |
4cb5073 |
dcbe030 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
301 |
2019-12-05T19:35:37+01:00 |
9576204 |
3bd56b9 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
Symbiotic |
4 |
2019-12-02 02:37:09 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62, sv-benchmarks/c/eca-rers2012/Problem14_label14_false-unreach-call_false-termination.c).
Found 15 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label14_false-unreach-call_false-termination.c, 738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
3010ecb |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2018-12-08T20:45 CET (sv-comp) |
|
8530aa8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Pinaka |
364 |
2018-12-07T12:16 CET (sv-comp) |
|
ae7a90c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
988 |
2018-12-07T06:32:20+01:00 |
|
da53b61 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
986 |
2018-12-09T18:15:50+01:00 |
8d77e38 |
4d34dee |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
986 |
2018-12-08T08:31:09+01:00 |
ae7a90c |
c2e399a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
1212 |
2018-12-07T17:11:22+01:00 |
8530aa8 |
4f3842d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
986 |
2018-12-06T09:48:44+01:00 |
387b73e |
5d29f50 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
1212 |
2018-12-06T09:12:15+01:00 |
feef18f |
387b73e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
986 |
2018-12-06T06:50:35+01:00 |
|
e181efd |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-10T20:39:09+01:00 |
1cf74c7 |
2f02a55 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-09T20:37:46+01:00 |
ffb961b |
4da7f59 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-08T23:45:16+01:00 |
3010ecb |
1130d64 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-08T05:04:47+01:00 |
481dfec |
fc3a096 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-06T10:19:58+01:00 |
1697482 |
acab976 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-06T09:41:43+01:00 |
7937139 |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62, sv-benchmarks/c/eca-rers2012/Problem14_label14_false-unreach-call_false-termination.c).
Found 13 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label14_false-unreach-call_false-termination.c, 738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
2285d81 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Veriabs |
5 |
2017-12-03T02:20 CET (sv-comp) |
|
011419f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2017-12-02T12:48 CET (sv-comp) |
|
fb821f0 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
7 |
2017-12-02T00:58:18.106917 |
|
ead4c08 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
7 |
2017-12-01T19:03:13.671097 |
|
3373d3b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
19 |
2017-12-01T16:03 CET (sv-comp) |
|
d09a9e4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
19 |
2017-12-01T02:50 CET (sv-comp) |
|
538ba56 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
522 |
2017-11-30T16:27:00+01:00 |
|
4c0ef09 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26758M |
714 |
2017-11-30T19:49:20+01:00 |
|
b4aca68 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26725 |
521 |
2017-11-30T13:53:27+01:00 |
|
ddb388b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
408 |
2017-11-30T19:42 CET (sv-comp) |
|
e881dd4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
2LS |
412 |
2017-12-01T02:44 CET (sv-comp) |
|
9bfdfd5 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
Automizer |
147 |
2017-12-03T11:13Z |
|
037eea0 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
2LS |
577 |
2017-12-01T15:07 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62, sv-benchmarks/c/eca-rers2012/Problem14_label14_false-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label14_false-unreach-call_false-termination.c, 738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/738ad3ec11184a8a57045e4298c70856e85ecfe1ce0594edb3adbb1d32a59c62.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |