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_label41_false-unreach-call_false-termination.c |
programSHA |
43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e |
witnessName |
results-verified/2ls.2017-12-01_1141.logfiles/sv-comp18.Problem14_label41_false-unreach-call_false-termination.c.files/witness.graphml |
witnessSHA |
c4684282f1ce8a58ae36f488ff60d6e27b0ccf21960c17089413db1139f2bc10 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/c4684282f1ce8a58ae36f488ff60d6e27b0ccf21960c17089413db1139f2bc10.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-01T12:53 CET (sv-comp) |
producer |
2LS |
program-sha256 |
43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e |
programfile |
../../sv-benchmarks/c/eca-rers2012/Problem14_label41_false-unreach-call_false-termination.c |
programhash |
8afc12ef0f10ef3dd28a2609b745763951bf0186 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(F end) ) |
witness-file |
witnessFileByHash/c4684282f1ce8a58ae36f488ff60d6e27b0ccf21960c17089413db1139f2bc10.graphml |
witness-sha256 |
c4684282f1ce8a58ae36f488ff60d6e27b0ccf21960c17089413db1139f2bc10 |
witness-size |
577226 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e, sv-benchmarks/c/eca-rers2012/Problem14_label41_false-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label41_false-unreach-call_false-termination.c, 43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e.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 (43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e, sv-benchmarks/c/eca-rers2012/Problem14_label41_false-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label41_false-unreach-call_false-termination.c, 43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e.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 (43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e, sv-benchmarks/c/eca-rers2012/Problem14_label41_false-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label41_false-unreach-call_false-termination.c, 43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e.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 (43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e, sv-benchmarks/c/eca-rers2012/Problem14_label41_false-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label41_false-unreach-call_false-termination.c, 43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e.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 (43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e, sv-benchmarks/c/eca-rers2012/Problem14_label41_false-unreach-call_false-termination.c).
Found 11 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label41_false-unreach-call_false-termination.c, 43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
ab292bc |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
4 |
2019-12-01 04:52:58 |
|
fcefcdb |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Pinaka |
405 |
2019-12-04T01:17 CET (comp) |
|
af00d8a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
1304 |
2019-12-11T21:09:08+01:00 |
ab292bc |
30e026b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
1304 |
2019-12-11T20:44:31+01:00 |
1bf8917 |
9b0b163 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
1628 |
2019-12-04T02:58:11+01:00 |
fcefcdb |
a2d413c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
1304 |
2019-12-03T08:08:53+01:00 |
b0c20b3 |
b0c20b3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
1303 |
2019-11-29T16:54:06+01:00 |
|
fb575ec |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
301 |
2019-12-11T20:55:21+01:00 |
b6dab2a |
956cf18 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
301 |
2019-12-07T21:19:47+01:00 |
1fad0bf |
508a3c1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
301 |
2019-12-05T20:21:22+01:00 |
9d55fb2 |
f119259 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
Symbiotic |
4 |
2019-12-01 14:26:31 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e, sv-benchmarks/c/eca-rers2012/Problem14_label41_false-unreach-call_false-termination.c).
Found 13 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label41_false-unreach-call_false-termination.c, 43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
f68bdbd |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2018-12-08T09:53 CET (sv-comp) |
|
9a6dcb1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Pinaka |
473 |
2018-12-06T23:00 CET (sv-comp) |
|
2788527 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
1311 |
2018-12-07T21:50:44+01:00 |
|
cc78929 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
1467 |
2018-12-09T18:21:27+01:00 |
45a68af |
8315a45 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
1304 |
2018-12-08T07:56:59+01:00 |
2788527 |
d96b6cf |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
1628 |
2018-12-07T17:44:54+01:00 |
9a6dcb1 |
bd0afa2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
1304 |
2018-12-06T09:49:10+01:00 |
1e390ca |
06da6aa |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
1843 |
2018-12-06T09:18:25+01:00 |
f025d2b |
1e390ca |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
1303 |
2018-12-05T10:32:47+01:00 |
|
b52eaee |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-10T20:39:34+01:00 |
c39e5bf |
731f071 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-08T23:43:32+01:00 |
f68bdbd |
b26d603 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-08T05:06:07+01:00 |
65e4ecc |
8da2d6d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-06T10:19:01+01:00 |
6d1ec91 |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e, sv-benchmarks/c/eca-rers2012/Problem14_label41_false-unreach-call_false-termination.c).
Found 13 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label41_false-unreach-call_false-termination.c, 43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
1b36b3b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
VeriAbs 1.3 |
719 |
Sat Dec 2 20:01:26 2017 |
|
50917ac |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2017-12-02T10:11 CET (sv-comp) |
|
fcce260 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
8 |
2017-12-01T18:47:57.921758 |
|
07d233e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
9 |
2017-12-01T09:02:17.977243 |
|
4450aa0 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
23 |
2017-12-01T17:04 CET (sv-comp) |
|
0838093 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
701 |
2017-11-30T12:20:01+01:00 |
|
d93ae28 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26758M |
927 |
2017-11-30T14:21:15+01:00 |
|
187dd86 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26725 |
699 |
2017-11-30T12:33:35+01:00 |
|
2a3d884 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
531 |
2017-11-30T23:36 CET (sv-comp) |
|
b96242f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Automizer |
997 |
2017-12-02T00:39Z |
|
f5a5942 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
2LS |
536 |
2017-11-30T14:21 CET (sv-comp) |
|
09e2317 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
Automizer |
147 |
2017-12-03T11:16Z |
|
c468428 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
2LS |
577 |
2017-12-01T12:53 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e, sv-benchmarks/c/eca-rers2012/Problem14_label41_false-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label41_false-unreach-call_false-termination.c, 43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/43d7bea03f9e8070e1e896137ff6df84c14f01030cf971a763ced6df0c8a131e.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |