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).
Key | Value |
programName | sv-benchmarks/c/product-lines/elevator_spec1_product20_false-unreach-call_true-termination.cil.c |
programSHA | 1cb2e490a36be92fe7ebf4e6173d7beace0fda7c341070fc9218ea507fbd7072 |
witnessName | results-verified/2ls.2018-12-04_2244.logfiles/sv-comp19_prop-reachsafety.elevator_spec1_product20_false-unreach-call_true-termination.cil.c.files/witness.graphml |
witnessSHA | 6339c0066e6c06c3c174679f509da4e65d298c70958da2749d6cf88d52bd7a1b |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-05T21:46 CET (sv-comp) |
producer | 2LS |
programfile | ../../sv-benchmarks/c/product-lines/elevator_spec1_product20_false-unreach-call_true-termination.cil.c |
programhash | d9c8d96fa066b936760c08808baca1cb90cf1092 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/6339c0066e6c06c3c174679f509da4e65d298c70958da2749d6cf88d52bd7a1b.graphml |
witness-sha256 | 6339c0066e6c06c3c174679f509da4e65d298c70958da2749d6cf88d52bd7a1b |
witness-size | 130953 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec1_product20_false-unreach-call_true-termination.cil.c, 1cb2e490a36be92fe7ebf4e6173d7beace0fda7c341070fc9218ea507fbd7072
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/1cb2e490a36be92fe7ebf4e6173d7beace0fda7c341070fc9218ea507fbd7072.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec1_product20_false-unreach-call_true-termination.cil.c, 1cb2e490a36be92fe7ebf4e6173d7beace0fda7c341070fc9218ea507fbd7072
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/1cb2e490a36be92fe7ebf4e6173d7beace0fda7c341070fc9218ea507fbd7072.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec1_product20_false-unreach-call_true-termination.cil.c, 1cb2e490a36be92fe7ebf4e6173d7beace0fda7c341070fc9218ea507fbd7072
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/1cb2e490a36be92fe7ebf4e6173d7beace0fda7c341070fc9218ea507fbd7072.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec1_product20_false-unreach-call_true-termination.cil.c, 1cb2e490a36be92fe7ebf4e6173d7beace0fda7c341070fc9218ea507fbd7072
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/1cb2e490a36be92fe7ebf4e6173d7beace0fda7c341070fc9218ea507fbd7072.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 15 witnesses for program sv-benchmarks/c/product-lines/elevator_spec1_product20_false-unreach-call_true-termination.cil.c, 1cb2e490a36be92fe7ebf4e6173d7beace0fda7c341070fc9218ea507fbd7072
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/1cb2e490a36be92fe7ebf4e6173d7beace0fda7c341070fc9218ea507fbd7072.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
fd04ab6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-01 22:34:01 | ||
75e52f7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 125 | 2019-12-03T22:04 CET (comp) | ||
4ad7c9e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 220 | 2019-12-11T21:40:42+01:00 | 4f268ac | |
84ff041 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 221 | 2019-12-11T21:09:19+01:00 | fd04ab6 | |
608be91 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 220 | 2019-12-11T20:54:55+01:00 | 2d25996 | |
7f69225 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 221 | 2019-12-11T20:44:28+01:00 | 821d0fd | |
4335982 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 220 | 2019-12-04T02:58:23+01:00 | 75e52f7 | |
e667cf3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 220 | 2019-12-03T08:57:42+01:00 | 7a39bc3 | |
c7a2bea | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 220 | 2019-12-03T08:09:04+01:00 | 3537564 | |
3537564 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 201 | 2019-11-30T07:47:34+01:00 | ||
4f268ac | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 220 | 2019-12-01T00:20:47+01:00 | ||
6a8fb30 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 305 | 2019-12-08T01:52:18+01:00 | f02626d | |
37adfd9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 305 | 2019-12-05T20:20:16+01:00 | 9e55615 | |
3e63fd2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 305 | 2019-12-05T19:34:39+01:00 | fc558ac | |
0140f0d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:50 CET (comp) |
Found 21 witnesses for program sv-benchmarks/c/product-lines/elevator_spec1_product20_false-unreach-call_true-termination.cil.c, 1cb2e490a36be92fe7ebf4e6173d7beace0fda7c341070fc9218ea507fbd7072
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/1cb2e490a36be92fe7ebf4e6173d7beace0fda7c341070fc9218ea507fbd7072.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
dfbf1b7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T04:53 CET (sv-comp) | ||
289457c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 32 | 2018-12-08T04:30:07 | ||
31b0655 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 142 | 2018-12-07T01:45 CET (sv-comp) | ||
e129422 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 227 | 2018-12-08T04:35:58+01:00 | ||
8790fbb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 220 | 2018-12-10T10:48:48+01:00 | ce88d1d | |
713bcb7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 221 | 2018-12-09T18:20:03+01:00 | becd536 | |
c863ed1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 220 | 2018-12-08T23:44:44+01:00 | dfbf1b7 | |
0925943 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 153 | 2018-12-08T22:09:55+01:00 | 289457c | |
86e1cca | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 220 | 2018-12-08T08:26:21+01:00 | e129422 | |
f2cfa93 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 220 | 2018-12-08T04:57:09+01:00 | 81273c1 | |
02863ca | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 220 | 2018-12-08T04:36:13+01:00 | ce88d1d | |
f91f81b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 220 | 2018-12-07T17:44:03+01:00 | 31b0655 | |
b80e7ac | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 220 | 2018-12-06T10:19:49+01:00 | e2da590 | |
6ac6713 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 220 | 2018-12-06T09:48:14+01:00 | 56878e0 | |
56878e0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 201 | 2018-12-06T04:43:36+01:00 | ||
1cca5af | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 305 | 2018-12-10T20:36:24+01:00 | e40c743 | |
2b575a5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 305 | 2018-12-06T09:41:44+01:00 | 6339c00 | |
3861db5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 305 | 2018-12-06T09:19:00+01:00 | 8cf4103 | |
55c7256 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 305 | 2018-12-06T09:18:14+01:00 | 3b11f00 | |
5b53a87 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T17:00 CET (sv-comp) | ||
e89a9ab | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T05:19 CET (sv-comp) |
Found 12 witnesses for program sv-benchmarks/c/product-lines/elevator_spec1_product20_false-unreach-call_true-termination.cil.c, 1cb2e490a36be92fe7ebf4e6173d7beace0fda7c341070fc9218ea507fbd7072
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/1cb2e490a36be92fe7ebf4e6173d7beace0fda7c341070fc9218ea507fbd7072.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a983bed | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T03:46 CET (sv-comp) | ||
a1a5941 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T01:21:36.163231 | ||
74b41e3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T13:23:51.372206 | ||
62e3e93 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 65 | 2017-12-01T18:32 CET (sv-comp) | ||
56867dd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 65 | 2017-11-30T17:21 CET (sv-comp) | ||
193fd61 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 180 | 2017-11-30T13:29:25+01:00 | ||
2c1ae72 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 113 | 2017-12-01T02:01 CET (sv-comp) | ||
ebff8b5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 131 | 2017-11-30T12:00 CET (sv-comp) | ||
d71c187 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T01:17:18.823380 | ||
35d4f56 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T09:23:24.135189 | ||
b69795e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 104 | 2017-12-01T14:59 CET (sv-comp) | ||
2bbc086 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 7024 | 2017-12-01T12:06 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec1_product20_false-unreach-call_true-termination.cil.c, 1cb2e490a36be92fe7ebf4e6173d7beace0fda7c341070fc9218ea507fbd7072
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/1cb2e490a36be92fe7ebf4e6173d7beace0fda7c341070fc9218ea507fbd7072.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |