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/bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c |
programSHA |
24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7 |
witnessName |
results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c.files/witness.graphml |
witnessSHA |
5268250f7d6a901cb9c5f6d4d2d91c30e55d4d6c9737670a86b4e3bc9da32b8b |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/5268250f7d6a901cb9c5f6d4d2d91c30e55d4d6c9737670a86b4e3bc9da32b8b.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-11-30T19:48 CET (sv-comp) |
memoryModel |
precise |
producer |
ESBMC 3.1 |
program-sha256 |
24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_c3d1dfb0-1127-4b1e-a043-1559a95a9c62/sv-benchmarks/c/bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c |
programhash |
602d5d97ec9296643fe5f445441afff0f98cd12a |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/5268250f7d6a901cb9c5f6d4d2d91c30e55d4d6c9737670a86b4e3bc9da32b8b.graphml |
witness-sha256 |
5268250f7d6a901cb9c5f6d4d2d91c30e55d4d6c9737670a86b4e3bc9da32b8b |
witness-size |
571609 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7, sv-benchmarks/c/bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c).
Found 0 witnesses for program sv-benchmarks/c/bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c, 24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7.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 (24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7, sv-benchmarks/c/bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c).
Found 0 witnesses for program sv-benchmarks/c/bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c, 24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7.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 (24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7, sv-benchmarks/c/bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c).
Found 0 witnesses for program sv-benchmarks/c/bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c, 24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7.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 (24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7, sv-benchmarks/c/bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c).
Found 0 witnesses for program sv-benchmarks/c/bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c, 24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7.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 (24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7, sv-benchmarks/c/bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c).
Found 12 witnesses for program sv-benchmarks/c/bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c, 24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
439de5f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
Pinaka |
13 |
2019-12-03T23:59 CET (comp) |
|
e35d69c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 1.9 |
15 |
2019-12-11T21:54:15+01:00 |
06c3ec4 |
f368211 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 1.9 |
15 |
2019-12-11T21:52:34+01:00 |
cac003f |
a56b8a7 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 1.9 |
16 |
2019-12-08T00:26:06+01:00 |
bb1429a |
8235737 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 1.9 |
15 |
2019-12-07T21:16:23+01:00 |
45341a9 |
befd259 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 1.9 |
16 |
2019-12-04T02:58:28+01:00 |
439de5f |
f3591a4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 1.9 |
15 |
2019-12-03T08:05:25+01:00 |
c980e72 |
c980e72 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 1.9 |
15 |
2019-11-30T07:03:51+01:00 |
|
cac003f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ |
15 |
2019-12-01T16:14:16+01:00 |
|
f9ee0db |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 1.9 |
53 |
2019-12-11T20:54:26+01:00 |
9194180 |
143fefb |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 1.9 |
53 |
2019-12-05T20:20:32+01:00 |
26c34bf |
38669cd |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 1.9 |
53 |
2019-12-05T19:34:10+01:00 |
e86aa10 |
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7, sv-benchmarks/c/bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c).
Found 6 witnesses for program sv-benchmarks/c/bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c, 24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
a1786e2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
SMACK 1.9.3 |
3 |
2018-12-08T10:28:29 |
|
bf4c01a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
127 |
2018-12-08T03:58:02+01:00 |
|
cafbb95 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
53 |
2018-12-08T22:00:34+01:00 |
a1786e2 |
c9f3ce1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
53 |
2018-12-08T05:40:32+01:00 |
bf4c01a |
122bb2a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
129 |
2018-12-06T09:30:43+01:00 |
e9c53d3 |
e9c53d3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
149 |
2018-12-06T03:54:08+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7, sv-benchmarks/c/bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c).
Found 2 witnesses for program sv-benchmarks/c/bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c, 24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
5268250 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 3.1 |
572 |
2017-11-30T19:48 CET (sv-comp) |
|
9aabbad |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
54 |
2017-12-01T08:28:58+01:00 |
3e208a5 |
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7, sv-benchmarks/c/bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c).
Found 0 witnesses for program sv-benchmarks/c/bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c, 24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/24913a192e75cf93e85014f6235b05cad44719897a59a58ad8505307a77deeb7.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |