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_label27_false-unreach-call.c |
programSHA |
0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a |
witnessName |
results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.Problem03_label27_false-unreach-call.c.files/witness.graphml |
witnessSHA |
8b0f4774f40620bf87fa08fca94be86d36f362fc96f3e1009856a44eb8085fda |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/8b0f4774f40620bf87fa08fca94be86d36f362fc96f3e1009856a44eb8085fda.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-02T06:13 CET (sv-comp) |
producer |
Symbiotic |
program-sha256 |
0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_d2de0570-316a-476a-a169-607ccec9e2a4/sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c |
programhash |
4b0a0f778efa43429684de6acf0eda5b289d9868 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/8b0f4774f40620bf87fa08fca94be86d36f362fc96f3e1009856a44eb8085fda.graphml |
witness-sha256 |
8b0f4774f40620bf87fa08fca94be86d36f362fc96f3e1009856a44eb8085fda |
witness-size |
1237 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a, sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c, 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a.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 (0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a, sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c, 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a.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 (0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a, sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c, 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a.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 (0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a, sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c, 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a.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 (0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a, sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c).
Found 12 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c, 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
6353eb1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
2 |
2019-12-01 08:35:14 |
|
e4a663c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Pinaka |
117 |
2019-12-03T22:21 CET (comp) |
|
7d0ffb3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
390 |
2019-12-11T21:41:19+01:00 |
1370e65 |
38494fd |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
390 |
2019-12-11T21:09:37+01:00 |
6353eb1 |
f1bf77a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
390 |
2019-12-11T20:54:49+01:00 |
872e57c |
cf5aff9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
390 |
2019-12-11T20:44:30+01:00 |
394b040 |
8a0b3b1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
391 |
2019-12-08T01:52:26+01:00 |
be52c73 |
9c224db |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
518 |
2019-12-04T02:58:19+01:00 |
e4a663c |
5173b8b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
390 |
2019-12-03T08:08:51+01:00 |
aaae5e4 |
aaae5e4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
390 |
2019-11-30T14:51:25+01:00 |
|
1370e65 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
390 |
2019-12-01T17:55:31+01:00 |
|
6afa3dd |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
685 |
2019-12-07T21:14:13+01:00 |
2321e4f |
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a, sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c).
Found 16 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c, 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
4de3834 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2018-12-08T10:10 CET (sv-comp) |
|
acd413f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
11 |
2018-12-08T03:48:05 |
|
8a9969f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Pinaka |
127 |
2018-12-07T10:34 CET (sv-comp) |
|
4abc341 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
394 |
2018-12-07T23:14:35+01:00 |
|
dfd7038 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
391 |
2018-12-10T20:38:02+01:00 |
14be678 |
4b84823 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
390 |
2018-12-09T18:21:35+01:00 |
5548683 |
87b8475 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
393 |
2018-12-08T23:44:07+01:00 |
4de3834 |
d435a22 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
390 |
2018-12-08T22:10:35+01:00 |
acd413f |
222e3d4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
390 |
2018-12-08T08:05:17+01:00 |
4abc341 |
210e882 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
390 |
2018-12-08T05:01:49+01:00 |
b3e6422 |
965ff6a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
518 |
2018-12-07T17:43:18+01:00 |
8a9969f |
92a0f3b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
390 |
2018-12-06T10:18:13+01:00 |
c6d1c55 |
ba76f22 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
390 |
2018-12-06T09:48:55+01:00 |
4955ba3 |
ef08a78 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
518 |
2018-12-06T09:20:07+01:00 |
830ddba |
4955ba3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
390 |
2018-12-06T05:04:45+01:00 |
|
ade1af7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
685 |
2018-12-09T20:54:34+01:00 |
e1c5b6e |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a, sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c).
Found 9 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c, 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
5762904 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Veriabs |
3 |
2017-12-02T22:55 CET (sv-comp) |
|
8b0f477 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2017-12-02T06:13 CET (sv-comp) |
|
18adfe2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
5 |
2017-12-01T12:40:42.702609 |
|
3c5389b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
5 |
2017-12-01T12:04:06.452187 |
|
14a0381 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
19 |
2017-12-01T00:32 CET (sv-comp) |
|
381b08e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
223 |
2017-11-30T18:00:55+01:00 |
|
9d3ee3f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26758M |
833 |
2017-12-01T00:05:25+01:00 |
|
1bc95fd |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
144 |
2017-11-30T12:23 CET (sv-comp) |
|
ab12923 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
2LS |
145 |
2017-11-30T19:08 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a, sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label27_false-unreach-call.c, 0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/0021eb9bf9450563b56e4bba87bf7c350236f1e69692a550e71072535e8a5c2a.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |