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/loops/s3_false-unreach-call.i |
programSHA |
c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e |
witnessName |
results-verified/2ls.2018-12-04_2244.logfiles/sv-comp19_prop-reachsafety.s3_false-unreach-call.i.files/witness.graphml |
witnessSHA |
4a9d477bdf0a4a9c0c6eb03ae3dde10d64e0e10012b7da2acaf91502d3b35f59 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/4a9d477bdf0a4a9c0c6eb03ae3dde10d64e0e10012b7da2acaf91502d3b35f59.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-06T03:40 CET (sv-comp) |
producer |
2LS |
programfile |
../../sv-benchmarks/c/loops/s3_false-unreach-call.i |
programhash |
cdf0cf9bd7de1f69825d4535f203da45c4edbbfc |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/4a9d477bdf0a4a9c0c6eb03ae3dde10d64e0e10012b7da2acaf91502d3b35f59.graphml |
witness-sha256 |
4a9d477bdf0a4a9c0c6eb03ae3dde10d64e0e10012b7da2acaf91502d3b35f59 |
witness-size |
39827 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e, sv-benchmarks/c/loops/s3_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/loops/s3_false-unreach-call.i, c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e.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 (c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e, sv-benchmarks/c/loops/s3_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/loops/s3_false-unreach-call.i, c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e.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 (c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e, sv-benchmarks/c/loops/s3_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/loops/s3_false-unreach-call.i, c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e.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 (c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e, sv-benchmarks/c/loops/s3_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/loops/s3_false-unreach-call.i, c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e.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 (c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e, sv-benchmarks/c/loops/s3_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/loops/s3_false-unreach-call.i, c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e.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 '19
Trying to find witnesses for program (c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e, sv-benchmarks/c/loops/s3_false-unreach-call.i).
Found 12 witnesses for program sv-benchmarks/c/loops/s3_false-unreach-call.i, c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
70326cf |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
8 |
2018-12-08T07:37:58 |
|
b2d43c4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7 |
73 |
2018-12-10T17:26:33+01:00 |
|
1efef58 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
102 |
2018-12-08T00:33:54+01:00 |
|
5a0f7a8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
82 |
2018-12-08T22:08:35+01:00 |
70326cf |
301f262 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
106 |
2018-12-08T08:17:10+01:00 |
1efef58 |
a0a958a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
106 |
2018-12-08T04:58:43+01:00 |
354273a |
0a75581 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
106 |
2018-12-06T10:11:00+01:00 |
23aad69 |
7c01324 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
106 |
2018-12-06T09:47:57+01:00 |
74eaee8 |
9959c47 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
107 |
2018-12-06T09:16:20+01:00 |
d54a0ac |
74eaee8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
103 |
2018-12-05T12:33:01+01:00 |
|
0650a20 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
48 |
2018-12-10T20:34:50+01:00 |
b2d43c4 |
ebea31f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
48 |
2018-12-06T09:41:58+01:00 |
4a9d477 |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e, sv-benchmarks/c/loops/s3_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/loops/s3_false-unreach-call.i, c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e.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 '17
Trying to find witnesses for program (c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e, sv-benchmarks/c/loops/s3_false-unreach-call.i).
Found 0 witnesses for program sv-benchmarks/c/loops/s3_false-unreach-call.i, c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/c3c460742e81ccc56593c4575f6aca1fb690d9f1632ba6271988f2b61d00132e.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |