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_product18_false-unreach-call_true-termination.cil.c |
programSHA | 4aae7fd50cf1cbcef6b2c8e1c4e81ca67635e13e1d65db8c70eeac8a15069589 |
witnessName | results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-reachsafety.elevator_spec2_product18_false-unreach-call_true-termination.cil.c.files/witness.graphml |
witnessSHA | 5ddcd1d0f77abfd7a0220e6726307ddb4153c55d45aede25a3613b36e8d648c5 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-05T17:55:41.451156 |
producer | DepthK v3.0 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_887e6008-6f4a-4038-befb-9a27b9130f58/sv-benchmarks/c/product-lines/elevator_spec2_product18_false-unreach-call_true-termination.cil.c |
programhash | fc7d4fa32c225e9bde4f412637f12e9da3676853 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/5ddcd1d0f77abfd7a0220e6726307ddb4153c55d45aede25a3613b36e8d648c5.graphml |
witness-sha256 | 5ddcd1d0f77abfd7a0220e6726307ddb4153c55d45aede25a3613b36e8d648c5 |
witness-size | 3705 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec2_product18_false-unreach-call_true-termination.cil.c, 4aae7fd50cf1cbcef6b2c8e1c4e81ca67635e13e1d65db8c70eeac8a15069589
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/4aae7fd50cf1cbcef6b2c8e1c4e81ca67635e13e1d65db8c70eeac8a15069589.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_product18_false-unreach-call_true-termination.cil.c, 4aae7fd50cf1cbcef6b2c8e1c4e81ca67635e13e1d65db8c70eeac8a15069589
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/4aae7fd50cf1cbcef6b2c8e1c4e81ca67635e13e1d65db8c70eeac8a15069589.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_product18_false-unreach-call_true-termination.cil.c, 4aae7fd50cf1cbcef6b2c8e1c4e81ca67635e13e1d65db8c70eeac8a15069589
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/4aae7fd50cf1cbcef6b2c8e1c4e81ca67635e13e1d65db8c70eeac8a15069589.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_product18_false-unreach-call_true-termination.cil.c, 4aae7fd50cf1cbcef6b2c8e1c4e81ca67635e13e1d65db8c70eeac8a15069589
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/4aae7fd50cf1cbcef6b2c8e1c4e81ca67635e13e1d65db8c70eeac8a15069589.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_spec2_product18_false-unreach-call_true-termination.cil.c, 4aae7fd50cf1cbcef6b2c8e1c4e81ca67635e13e1d65db8c70eeac8a15069589
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/4aae7fd50cf1cbcef6b2c8e1c4e81ca67635e13e1d65db8c70eeac8a15069589.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d159366 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-01 01:20:00 | ||
8c7be58 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 106 | 2019-12-04T00:20 CET (comp) | ||
a3a6ae5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 191 | 2019-12-11T21:42:27+01:00 | d677683 | |
c7ce4e9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 191 | 2019-12-11T21:09:26+01:00 | d159366 | |
6fd34c4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 191 | 2019-12-11T20:54:26+01:00 | 9519f77 | |
4679ca9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 191 | 2019-12-11T20:44:31+01:00 | 775d2c0 | |
42c4c27 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 191 | 2019-12-08T01:51:27+01:00 | 518f91c | |
215f804 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 191 | 2019-12-04T02:58:04+01:00 | 8c7be58 | |
e7d666e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 191 | 2019-12-03T08:57:15+01:00 | f1bd81e | |
168416b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 191 | 2019-12-03T08:09:59+01:00 | 110c345 | |
110c345 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 176 | 2019-11-30T14:31:12+01:00 | ||
518f91c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 194 | 2019-12-07T19:12:14+01:00 | ||
d677683 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 190 | 2019-12-01T05:34:54+01:00 | ||
befbe91 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 297 | 2019-12-05T20:20:39+01:00 | 6e08542 | |
fc2989e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 297 | 2019-12-05T19:34:36+01:00 | 77a2f1c | |
0c5b251 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:40 CET (comp) |
Found 22 witnesses for program sv-benchmarks/c/product-lines/elevator_spec2_product18_false-unreach-call_true-termination.cil.c, 4aae7fd50cf1cbcef6b2c8e1c4e81ca67635e13e1d65db8c70eeac8a15069589
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/4aae7fd50cf1cbcef6b2c8e1c4e81ca67635e13e1d65db8c70eeac8a15069589.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9bf8ab5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T08:48 CET (sv-comp) | ||
0710104 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 27 | 2018-12-08T00:32:41 | ||
58b952e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 121 | 2018-12-07T06:39 CET (sv-comp) | ||
19935d1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 175 | 2018-12-10T18:38:18+01:00 | ||
0cf9e6b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 196 | 2018-12-08T02:53:55+01:00 | ||
7e7bac6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 191 | 2018-12-10T20:37:58+01:00 | 19935d1 | |
cceccb0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 191 | 2018-12-10T10:48:44+01:00 | daf2d3a | |
aa3db69 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 191 | 2018-12-09T17:48:56+01:00 | 4b8fa7c | |
46c316f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 191 | 2018-12-08T23:42:07+01:00 | 9bf8ab5 | |
643c062 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 133 | 2018-12-08T22:10:37+01:00 | 0710104 | |
6bef9a9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 191 | 2018-12-08T07:52:04+01:00 | 0cf9e6b | |
3d65126 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 191 | 2018-12-08T05:02:49+01:00 | 83a12eb | |
e69966d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 191 | 2018-12-08T03:56:37+01:00 | daf2d3a | |
8147e4c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 191 | 2018-12-07T17:43:55+01:00 | 58b952e | |
36315f3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 191 | 2018-12-06T10:16:59+01:00 | 5ddcd1d | |
84a4844 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 191 | 2018-12-06T09:48:24+01:00 | 299eee9 | |
299eee9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 176 | 2018-12-05T21:35:23+01:00 | ||
6cccf45 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 297 | 2018-12-06T09:40:55+01:00 | a36716d | |
1311843 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 297 | 2018-12-06T09:19:32+01:00 | e94a5ce | |
dadf18e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 297 | 2018-12-06T09:15:42+01:00 | c14b738 | |
24c4a69 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T12:21 CET (sv-comp) | ||
7f32678 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T13:40 CET (sv-comp) |
Found 12 witnesses for program sv-benchmarks/c/product-lines/elevator_spec2_product18_false-unreach-call_true-termination.cil.c, 4aae7fd50cf1cbcef6b2c8e1c4e81ca67635e13e1d65db8c70eeac8a15069589
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/4aae7fd50cf1cbcef6b2c8e1c4e81ca67635e13e1d65db8c70eeac8a15069589.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
aa8c3b1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T09:07 CET (sv-comp) | ||
c3f24a5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-01T15:06:31.344890 | ||
2d50b0b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T13:09:52.891914 | ||
3e5c380 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 55 | 2017-12-01T17:30 CET (sv-comp) | ||
171c411 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 55 | 2017-12-01T02:25 CET (sv-comp) | ||
2755706 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 157 | 2017-11-30T15:37:31+01:00 | ||
6ab85c0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 98 | 2017-11-30T15:12 CET (sv-comp) | ||
389c054 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 113 | 2017-12-01T02:29 CET (sv-comp) | ||
bff6353 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T21:12:01.441495 | ||
4662bb6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T08:52:07.546174 | ||
e919794 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 90 | 2017-12-01T17:10 CET (sv-comp) | ||
06115cf | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 6662 | 2017-12-01T14:44 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec2_product18_false-unreach-call_true-termination.cil.c, 4aae7fd50cf1cbcef6b2c8e1c4e81ca67635e13e1d65db8c70eeac8a15069589
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/4aae7fd50cf1cbcef6b2c8e1c4e81ca67635e13e1d65db8c70eeac8a15069589.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |