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_spec2_product30_false-unreach-call_true-termination.cil.c |
programSHA | 4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009 |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-smack.2018-12-08_2205.logfiles/sv-comp19_prop-reachsafety.elevator_spec2_product30_false-unreach-call_true-termination.cil.c.files/witness.graphml |
witnessSHA | 053b6f247be5c3dfeaff905ae1866e6fcd4e5db2f8a17962aad4cca490685ea0 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T22:11:25+01:00 |
inputwitnesshash | 0942ae405137ef4aab3d5756ac7dc46792a475c511033f9b1e3b16d0aa7fc4af |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009 |
programfile | ../../sv-benchmarks/c/product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c |
programhash | 4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/053b6f247be5c3dfeaff905ae1866e6fcd4e5db2f8a17962aad4cca490685ea0.graphml |
witness-sha256 | 053b6f247be5c3dfeaff905ae1866e6fcd4e5db2f8a17962aad4cca490685ea0 |
witness-size | 139589 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, 4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009).
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c, 4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009.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_spec2_product30_false-unreach-call_true-termination.cil.c, 4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009.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_spec2_product30_false-unreach-call_true-termination.cil.c, 4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009.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_spec2_product30_false-unreach-call_true-termination.cil.c, 4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009.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_spec2_product30_false-unreach-call_true-termination.cil.c, 4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e57a25b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-01 20:33:25 | ||
75e64bf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 115 | 2019-12-04T00:25 CET (comp) | ||
8ec5e80 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 203 | 2019-12-11T21:40:10+01:00 | 4313af1 | |
8115d28 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 203 | 2019-12-11T21:09:03+01:00 | e57a25b | |
543e5f5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 203 | 2019-12-11T20:54:22+01:00 | d4d3091 | |
733d38c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 203 | 2019-12-11T20:44:45+01:00 | b567657 | |
d9481b1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 203 | 2019-12-04T02:58:20+01:00 | 75e64bf | |
aef1764 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 203 | 2019-12-03T08:57:03+01:00 | 1512a47 | |
2641b7a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 203 | 2019-12-03T08:08:32+01:00 | 6690764 | |
6690764 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 187 | 2019-11-30T12:09:28+01:00 | ||
4313af1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 187 | 2019-12-01T03:09:34+01:00 | ||
a12c249 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 314 | 2019-12-08T01:51:41+01:00 | 1e6edc0 | |
af2a080 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 314 | 2019-12-05T20:20:18+01:00 | a3a7d01 | |
81677c7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 314 | 2019-12-05T19:34:10+01:00 | 0800c46 | |
7c52c38 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:19 CET (comp) |
Found 21 witnesses for program sv-benchmarks/c/product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c, 4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
97d1217 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T00:08 CET (sv-comp) | ||
0942ae4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 30 | 2018-12-08T03:40:50 | ||
d401c67 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 130 | 2018-12-07T04:07 CET (sv-comp) | ||
750f355 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 209 | 2018-12-07T11:02:49+01:00 | ||
dfe3c99 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 203 | 2018-12-10T10:49:00+01:00 | a05304b | |
533da0a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 204 | 2018-12-09T18:20:21+01:00 | b33f93c | |
c123046 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 203 | 2018-12-08T23:42:57+01:00 | 97d1217 | |
053b6f2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 140 | 2018-12-08T22:11:25+01:00 | 0942ae4 | |
2303f5c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 203 | 2018-12-08T08:08:32+01:00 | 750f355 | |
f6638a8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 203 | 2018-12-08T05:01:45+01:00 | 10f4946 | |
8c8a6ae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 203 | 2018-12-08T04:28:23+01:00 | a05304b | |
4f8fd2c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 203 | 2018-12-07T17:44:26+01:00 | d401c67 | |
8174b65 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 203 | 2018-12-06T10:17:44+01:00 | a3c2de4 | |
a99e920 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 203 | 2018-12-06T09:47:57+01:00 | 61ba61c | |
61ba61c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 187 | 2018-12-05T10:09:51+01:00 | ||
336dd0f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 314 | 2018-12-10T20:38:07+01:00 | 6438b11 | |
8b7f882 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 314 | 2018-12-06T09:42:27+01:00 | 8ec064a | |
dfb2c98 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 314 | 2018-12-06T09:18:21+01:00 | df70a0c | |
b270890 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 314 | 2018-12-06T09:02:01+01:00 | 01070d7 | |
8fbb8c9 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T05:07 CET (sv-comp) | ||
c603820 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T06:39 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c, 4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009.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_spec2_product30_false-unreach-call_true-termination.cil.c, 4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/4f9c0d446c683bf57f8ba0a9ca884e97f65b7c47fe9d55b3bb71f96f33c68009.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |