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_spec3_product32_false-unreach-call_true-termination.cil.c |
programSHA | 9e41379e8c25ab1ab970362d85b2dbf4dc9460e1064510765fd35c4e3672459f |
witnessName | results-verified/smack.2018-12-07_1913.logfiles/sv-comp19_prop-reachsafety.elevator_spec3_product32_false-unreach-call_true-termination.cil.c.files/witness.graphml |
witnessSHA | 864ddf1f21f21d2f1cdc9280d4c30ce3d715ebc75b27852218981420f828e0d1 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T06:11:05 |
producer | SMACK 1.9.3 |
program-sha256 | 9e41379e8c25ab1ab970362d85b2dbf4dc9460e1064510765fd35c4e3672459f |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_f9924c2e-e07a-4295-a62c-8e262402c7c8/sv-benchmarks/c/product-lines/elevator_spec3_product32_false-unreach-call_true-termination.cil.c |
programhash | 9e41379e8c25ab1ab970362d85b2dbf4dc9460e1064510765fd35c4e3672459f |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/864ddf1f21f21d2f1cdc9280d4c30ce3d715ebc75b27852218981420f828e0d1.graphml |
witness-sha256 | 864ddf1f21f21d2f1cdc9280d4c30ce3d715ebc75b27852218981420f828e0d1 |
witness-size | 62430 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, 9e41379e8c25ab1ab970362d85b2dbf4dc9460e1064510765fd35c4e3672459f).
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec3_product32_false-unreach-call_true-termination.cil.c, 9e41379e8c25ab1ab970362d85b2dbf4dc9460e1064510765fd35c4e3672459f
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/9e41379e8c25ab1ab970362d85b2dbf4dc9460e1064510765fd35c4e3672459f.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_spec3_product32_false-unreach-call_true-termination.cil.c, 9e41379e8c25ab1ab970362d85b2dbf4dc9460e1064510765fd35c4e3672459f
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/9e41379e8c25ab1ab970362d85b2dbf4dc9460e1064510765fd35c4e3672459f.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_spec3_product32_false-unreach-call_true-termination.cil.c, 9e41379e8c25ab1ab970362d85b2dbf4dc9460e1064510765fd35c4e3672459f
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/9e41379e8c25ab1ab970362d85b2dbf4dc9460e1064510765fd35c4e3672459f.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_spec3_product32_false-unreach-call_true-termination.cil.c, 9e41379e8c25ab1ab970362d85b2dbf4dc9460e1064510765fd35c4e3672459f
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/9e41379e8c25ab1ab970362d85b2dbf4dc9460e1064510765fd35c4e3672459f.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_spec3_product32_false-unreach-call_true-termination.cil.c, 9e41379e8c25ab1ab970362d85b2dbf4dc9460e1064510765fd35c4e3672459f
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/9e41379e8c25ab1ab970362d85b2dbf4dc9460e1064510765fd35c4e3672459f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
aa5d251 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-02 03:40:19 | ||
e37c985 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 203 | 2019-12-03T22:46 CET (comp) | ||
5cf4045 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 349 | 2019-12-11T21:44:05+01:00 | f7778d6 | |
3369916 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 350 | 2019-12-11T21:09:21+01:00 | aa5d251 | |
e31a993 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 349 | 2019-12-11T20:54:54+01:00 | b9f3679 | |
0e4f987 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 350 | 2019-12-11T20:44:53+01:00 | d84198c | |
c897457 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 349 | 2019-12-08T01:51:20+01:00 | e64a386 | |
1c540c4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 349 | 2019-12-04T02:58:09+01:00 | e37c985 | |
6c93513 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 349 | 2019-12-03T08:57:09+01:00 | e6bb4c9 | |
299f97e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 349 | 2019-12-03T08:10:31+01:00 | 6edb6ff | |
6edb6ff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 308 | 2019-11-29T15:17:19+01:00 | ||
e64a386 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 351 | 2019-12-07T22:32:46+01:00 | ||
f7778d6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 348 | 2019-12-01T10:47:12+01:00 | ||
f0ccfce | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 328 | 2019-12-05T20:20:31+01:00 | ec52af7 | |
39d431a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 328 | 2019-12-05T19:34:28+01:00 | 8b146db | |
b804c7e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:52 CET (comp) |
Found 22 witnesses for program sv-benchmarks/c/product-lines/elevator_spec3_product32_false-unreach-call_true-termination.cil.c, 9e41379e8c25ab1ab970362d85b2dbf4dc9460e1064510765fd35c4e3672459f
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/9e41379e8c25ab1ab970362d85b2dbf4dc9460e1064510765fd35c4e3672459f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6a76b4d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T05:57 CET (sv-comp) | ||
864ddf1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 62 | 2018-12-08T06:11:05 | ||
f72ccdf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 230 | 2018-12-07T10:13 CET (sv-comp) | ||
8762a32 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 321 | 2018-12-10T18:55:20+01:00 | ||
657e815 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 350 | 2018-12-07T17:57:43+01:00 | ||
2482154 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 349 | 2018-12-10T20:37:10+01:00 | 8762a32 | |
4271474 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 349 | 2018-12-10T10:48:44+01:00 | aa9215c | |
2837b14 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 350 | 2018-12-09T18:20:19+01:00 | aa4b91b | |
471a402 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 349 | 2018-12-08T23:43:43+01:00 | 6a76b4d | |
ebce98e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 216 | 2018-12-08T22:11:24+01:00 | 864ddf1 | |
fd675bf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 349 | 2018-12-08T08:03:07+01:00 | 657e815 | |
a3225fe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 349 | 2018-12-08T04:57:30+01:00 | 6c1bd0a | |
57cb0c9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 349 | 2018-12-08T03:55:53+01:00 | aa9215c | |
bb6fe56 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 349 | 2018-12-07T17:43:04+01:00 | f72ccdf | |
f478ee3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 349 | 2018-12-06T10:20:14+01:00 | 9bfbd25 | |
81b336f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 349 | 2018-12-06T09:48:06+01:00 | 018b321 | |
018b321 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 308 | 2018-12-06T05:35:48+01:00 | ||
517bbeb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 328 | 2018-12-06T09:41:40+01:00 | 9a6a145 | |
c2f2ad7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 328 | 2018-12-06T09:19:44+01:00 | e13a536 | |
6dd561f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 328 | 2018-12-06T09:11:36+01:00 | 1866b46 | |
337db98 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T07:37 CET (sv-comp) | ||
8720f27 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T01:13 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec3_product32_false-unreach-call_true-termination.cil.c, 9e41379e8c25ab1ab970362d85b2dbf4dc9460e1064510765fd35c4e3672459f
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/9e41379e8c25ab1ab970362d85b2dbf4dc9460e1064510765fd35c4e3672459f.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_spec3_product32_false-unreach-call_true-termination.cil.c, 9e41379e8c25ab1ab970362d85b2dbf4dc9460e1064510765fd35c4e3672459f
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/9e41379e8c25ab1ab970362d85b2dbf4dc9460e1064510765fd35c4e3672459f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |