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/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c |
programSHA |
f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494 |
witnessName |
results-verified/verifuzz.2018-12-09_0247.logfiles/sv-comp19_prop-reachsafety.pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c.files/witness.graphml |
witnessSHA |
cc3373a95cebf73a9a18c93400a1a2f8d0991d581340ea5a110061cdaab7d5ae |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/cc3373a95cebf73a9a18c93400a1a2f8d0991d581340ea5a110061cdaab7d5ae.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-09T04:20 CET (sv-comp) |
memorymodel |
precise |
producer |
verifuzz |
programfile |
/home/benchexec/VERIFUZZ_TEMP_DIR/OUT/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c |
programhash |
81e95e3c6b86bd348b23483edbbca02aa109e1fc |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/cc3373a95cebf73a9a18c93400a1a2f8d0991d581340ea5a110061cdaab7d5ae.graphml |
witness-sha256 |
cc3373a95cebf73a9a18c93400a1a2f8d0991d581340ea5a110061cdaab7d5ae |
witness-size |
8336 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c, f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494.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 (f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c, f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494.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 (f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c, f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494.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 (f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c, f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494.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 (f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c).
Found 11 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c, f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
16a078e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Pinaka |
200 |
2019-12-04T00:14 CET (comp) |
|
4fc11a7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
293 |
2019-12-11T21:57:59+01:00 |
65f77fb |
94326d8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
296 |
2019-12-11T20:44:30+01:00 |
9a4c5b6 |
d28af04 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
293 |
2019-12-03T08:08:19+01:00 |
fd0f047 |
fd0f047 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
299 |
2019-11-30T10:08:48+01:00 |
|
65f77fb |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
295 |
2019-12-01T06:34:18+01:00 |
|
2c39207 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
53 |
2019-12-11T20:54:28+01:00 |
651dd76 |
e0a1a23 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
53 |
2019-12-08T01:51:35+01:00 |
d848c64 |
78673f3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
53 |
2019-12-05T20:21:48+01:00 |
0114bfb |
af00d95 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
53 |
2019-12-05T19:34:08+01:00 |
7356eac |
4b169cb |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
53 |
2019-12-04T02:58:04+01:00 |
16a078e |
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c).
Found 15 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c, f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
7ccad0a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
12 |
2018-12-08T09:31 CET (sv-comp) |
|
319c98d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
75 |
2018-12-08T12:11:46 |
|
4e564a5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
296 |
2018-12-07T02:48:11+01:00 |
|
caa1e45 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
296 |
2018-12-09T18:20:53+01:00 |
cc3373a |
47e076b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
295 |
2018-12-08T23:44:52+01:00 |
7ccad0a |
b735d33 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
293 |
2018-12-08T08:45:46+01:00 |
4e564a5 |
6680ce8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
293 |
2018-12-06T09:48:08+01:00 |
c9de031 |
c9de031 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
299 |
2018-12-05T15:40:04+01:00 |
|
a51c7bc |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
53 |
2018-12-10T20:37:03+01:00 |
7bacc7d |
8ae2f73 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
53 |
2018-12-08T22:11:28+01:00 |
319c98d |
91e82fe |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
53 |
2018-12-08T05:00:53+01:00 |
f8d0e59 |
6a553c8 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
53 |
2018-12-06T10:12:11+01:00 |
601bd53 |
03e3ddc |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
53 |
2018-12-06T09:40:47+01:00 |
f26a43b |
886946b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
53 |
2018-12-06T09:20:01+01:00 |
da89cee |
1a2758c |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
1 |
2018-12-08T20:19 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c).
Found 13 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c, f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
e8cbe48 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
VeriAbs 1.3 |
214 |
Sat Dec 2 20:53:14 2017 |
|
cb00a4b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
12 |
2017-12-02T09:45 CET (sv-comp) |
|
2dc24a5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
34 |
2017-12-01T17:07:45.404553 |
|
eb7f1a9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
34 |
2017-12-01T10:02:52.328048 |
|
89de9b1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
95 |
2017-12-01T16:59 CET (sv-comp) |
|
aae5be2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
91 |
2017-12-01T01:18 CET (sv-comp) |
|
0370d64 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
290 |
2017-11-30T15:46:21+01:00 |
|
b67dab0 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
225 |
2017-11-30T21:48 CET (sv-comp) |
|
3b22624 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
2LS |
185 |
2017-12-01T03:37 CET (sv-comp) |
|
745b378 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 |
3 |
2017-12-03T02:19:21.997251 |
|
d9f444f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 4.6.0 |
3 |
2017-12-02T08:44:11.333559 |
|
7f859a3 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
412 |
2017-12-01T13:24 CET (sv-comp) |
|
882894f |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
96 |
2017-12-01T13:06 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494, sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c).
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c, f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f2f10f88826d029b6a7947d59d7d1978e207067768bf5a14fb77c588af5a8494.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |