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_spec14_product24_false-unreach-call_true-termination.cil.c |
programSHA | 7784c714ef470aa5e5bb76f1077834ca7868c83d5de9c96f784d85127086dbc8 |
witnessName | results-verified/2ls.2018-12-04_2244.logfiles/sv-comp19_prop-reachsafety.elevator_spec14_product24_false-unreach-call_true-termination.cil.c.files/witness.graphml |
witnessSHA | 8f48c40ecf7f124245b8d624ca79e5386883a9f1e45fe6a1d23b97a93c83e02e |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-05T23:18 CET (sv-comp) |
producer | 2LS |
programfile | ../../sv-benchmarks/c/product-lines/elevator_spec14_product24_false-unreach-call_true-termination.cil.c |
programhash | 2fd90e89c0e98d2aa335e1695a5b9f6f2ec5e5af |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/8f48c40ecf7f124245b8d624ca79e5386883a9f1e45fe6a1d23b97a93c83e02e.graphml |
witness-sha256 | 8f48c40ecf7f124245b8d624ca79e5386883a9f1e45fe6a1d23b97a93c83e02e |
witness-size | 120921 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec14_product24_false-unreach-call_true-termination.cil.c, 7784c714ef470aa5e5bb76f1077834ca7868c83d5de9c96f784d85127086dbc8
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/7784c714ef470aa5e5bb76f1077834ca7868c83d5de9c96f784d85127086dbc8.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_spec14_product24_false-unreach-call_true-termination.cil.c, 7784c714ef470aa5e5bb76f1077834ca7868c83d5de9c96f784d85127086dbc8
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/7784c714ef470aa5e5bb76f1077834ca7868c83d5de9c96f784d85127086dbc8.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_spec14_product24_false-unreach-call_true-termination.cil.c, 7784c714ef470aa5e5bb76f1077834ca7868c83d5de9c96f784d85127086dbc8
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/7784c714ef470aa5e5bb76f1077834ca7868c83d5de9c96f784d85127086dbc8.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_spec14_product24_false-unreach-call_true-termination.cil.c, 7784c714ef470aa5e5bb76f1077834ca7868c83d5de9c96f784d85127086dbc8
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/7784c714ef470aa5e5bb76f1077834ca7868c83d5de9c96f784d85127086dbc8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 16 witnesses for program sv-benchmarks/c/product-lines/elevator_spec14_product24_false-unreach-call_true-termination.cil.c, 7784c714ef470aa5e5bb76f1077834ca7868c83d5de9c96f784d85127086dbc8
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/7784c714ef470aa5e5bb76f1077834ca7868c83d5de9c96f784d85127086dbc8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f6b06e1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-02 03:51:41 | ||
98d97d8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 115 | 2019-12-04T00:28 CET (comp) | ||
21e4456 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 203 | 2019-12-11T21:58:28+01:00 | e918d9f | |
879d86f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 204 | 2019-12-11T21:09:06+01:00 | f6b06e1 | |
e7ee081 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 203 | 2019-12-11T20:55:00+01:00 | 1704086 | |
eecc514 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 204 | 2019-12-11T20:44:50+01:00 | 266906b | |
d476e05 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 203 | 2019-12-08T01:51:49+01:00 | d806a5c | |
7012445 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 203 | 2019-12-04T02:58:31+01:00 | 98d97d8 | |
3dccaba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 203 | 2019-12-03T08:57:03+01:00 | e48a440 | |
e4e36e7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 203 | 2019-12-03T08:10:14+01:00 | f4a2ac5 | |
f4a2ac5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 186 | 2019-11-30T12:17:13+01:00 | ||
d806a5c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 206 | 2019-12-07T13:22:00+01:00 | ||
e918d9f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 186 | 2019-12-01T00:52:53+01:00 | ||
ec3867a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 300 | 2019-12-05T20:21:55+01:00 | 3a14246 | |
7b11620 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 300 | 2019-12-05T19:34:08+01:00 | c608485 | |
c3719c4 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-04T01:29 CET (comp) |
Found 22 witnesses for program sv-benchmarks/c/product-lines/elevator_spec14_product24_false-unreach-call_true-termination.cil.c, 7784c714ef470aa5e5bb76f1077834ca7868c83d5de9c96f784d85127086dbc8
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/7784c714ef470aa5e5bb76f1077834ca7868c83d5de9c96f784d85127086dbc8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d696f9c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T01:54 CET (sv-comp) | ||
6a28c67 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 29 | 2018-12-08T01:58:49 | ||
68d3e13 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 130 | 2018-12-07T01:29 CET (sv-comp) | ||
ced1e65 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 186 | 2018-12-10T18:03:07+01:00 | ||
d43b990 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 209 | 2018-12-07T10:59:11+01:00 | ||
3d837c2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 203 | 2018-12-10T20:34:53+01:00 | ced1e65 | |
2bdcb7e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 203 | 2018-12-10T10:48:50+01:00 | 850565c | |
bbd69fa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 204 | 2018-12-09T18:19:58+01:00 | c01c7ee | |
187f242 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 203 | 2018-12-08T23:43:34+01:00 | d696f9c | |
dff7a31 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 143 | 2018-12-08T22:10:37+01:00 | 6a28c67 | |
fb75c6f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 203 | 2018-12-08T08:25:40+01:00 | d43b990 | |
0df14fd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 203 | 2018-12-08T04:56:06+01:00 | 52c6a8a | |
1db132d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 203 | 2018-12-08T04:36:47+01:00 | 850565c | |
71e34c6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 203 | 2018-12-07T17:45:28+01:00 | 68d3e13 | |
b94a416 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 203 | 2018-12-06T10:20:11+01:00 | 9b1b9c2 | |
2191088 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 203 | 2018-12-06T09:49:10+01:00 | f638cad | |
f638cad | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 186 | 2018-12-06T03:42:58+01:00 | ||
f24bbad | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 300 | 2018-12-06T09:40:40+01:00 | 8f48c40 | |
16b0097 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 300 | 2018-12-06T09:17:48+01:00 | 9ed067b | |
62696a6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 300 | 2018-12-06T09:00:50+01:00 | 3d1360b | |
7c43cfe | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T16:17 CET (sv-comp) | ||
f815fa5 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-06T23:59 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec14_product24_false-unreach-call_true-termination.cil.c, 7784c714ef470aa5e5bb76f1077834ca7868c83d5de9c96f784d85127086dbc8
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/7784c714ef470aa5e5bb76f1077834ca7868c83d5de9c96f784d85127086dbc8.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_spec14_product24_false-unreach-call_true-termination.cil.c, 7784c714ef470aa5e5bb76f1077834ca7868c83d5de9c96f784d85127086dbc8
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/7784c714ef470aa5e5bb76f1077834ca7868c83d5de9c96f784d85127086dbc8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |