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_product09_true-unreach-call_true-termination.cil.c |
programSHA | abcc9b31d7d764cbd1d5e771eb5ec7db4c91cf0b5a8ad87f4976c474bc7b816a |
witnessName | results-verified/symbiotic.2018-12-07_2142.logfiles/sv-comp19_prop-reachsafety.elevator_spec2_product09_true-unreach-call_true-termination.cil.c.files/witness.graphml |
witnessSHA | 96db9d4f2601bc1eb7c24ea866ecde8fe39f662a6fb3e3cc03600712c7c3bda4 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T02:04 CET (sv-comp) |
producer | Symbiotic |
program-sha256 | abcc9b31d7d764cbd1d5e771eb5ec7db4c91cf0b5a8ad87f4976c474bc7b816a |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_52b7255a-ea37-42a0-b79a-4640901ff664/sv-benchmarks/c/product-lines/elevator_spec2_product09_true-unreach-call_true-termination.cil.c |
programhash | abcc9b31d7d764cbd1d5e771eb5ec7db4c91cf0b5a8ad87f4976c474bc7b816a |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/96db9d4f2601bc1eb7c24ea866ecde8fe39f662a6fb3e3cc03600712c7c3bda4.graphml |
witness-sha256 | 96db9d4f2601bc1eb7c24ea866ecde8fe39f662a6fb3e3cc03600712c7c3bda4 |
witness-size | 803 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, abcc9b31d7d764cbd1d5e771eb5ec7db4c91cf0b5a8ad87f4976c474bc7b816a).
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec2_product09_true-unreach-call_true-termination.cil.c, abcc9b31d7d764cbd1d5e771eb5ec7db4c91cf0b5a8ad87f4976c474bc7b816a
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/abcc9b31d7d764cbd1d5e771eb5ec7db4c91cf0b5a8ad87f4976c474bc7b816a.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_product09_true-unreach-call_true-termination.cil.c, abcc9b31d7d764cbd1d5e771eb5ec7db4c91cf0b5a8ad87f4976c474bc7b816a
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/abcc9b31d7d764cbd1d5e771eb5ec7db4c91cf0b5a8ad87f4976c474bc7b816a.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_product09_true-unreach-call_true-termination.cil.c, abcc9b31d7d764cbd1d5e771eb5ec7db4c91cf0b5a8ad87f4976c474bc7b816a
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/abcc9b31d7d764cbd1d5e771eb5ec7db4c91cf0b5a8ad87f4976c474bc7b816a.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_product09_true-unreach-call_true-termination.cil.c, abcc9b31d7d764cbd1d5e771eb5ec7db4c91cf0b5a8ad87f4976c474bc7b816a
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/abcc9b31d7d764cbd1d5e771eb5ec7db4c91cf0b5a8ad87f4976c474bc7b816a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 14 witnesses for program sv-benchmarks/c/product-lines/elevator_spec2_product09_true-unreach-call_true-termination.cil.c, abcc9b31d7d764cbd1d5e771eb5ec7db4c91cf0b5a8ad87f4976c474bc7b816a
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/abcc9b31d7d764cbd1d5e771eb5ec7db4c91cf0b5a8ad87f4976c474bc7b816a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2376815 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:16 CET (comp) | ||
10c0d94 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 291 | 2019-12-11T20:12:47+01:00 | c2f9005 | |
66635fb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 291 | 2019-12-11T20:08:15+01:00 | 61bd757 | |
bce9b0b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 291 | 2019-12-11T20:02:35+01:00 | 9db8ca7 | |
ad53c67 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 291 | 2019-12-08T00:36:38+01:00 | b7dd4e6 | |
7536ebc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 291 | 2019-12-05T19:18:06+01:00 | 04f755f | |
7cb0548 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 291 | 2019-12-05T19:03:17+01:00 | 7df7550 | |
d920912 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 291 | 2019-12-04T02:08:01+01:00 | 2376815 | |
3213766 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 291 | 2019-11-30T19:53:42+01:00 | b917b10 | |
aa4cc3e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 291 | 2019-11-30T17:00:09+01:00 | 60503ab | |
60503ab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 291 | 2019-11-30T06:30:17+01:00 | ||
b7dd4e6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8 | 291 | 2019-12-07T21:08:37+01:00 | ||
61bd757 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 291 | 2019-12-01T08:44:39+01:00 | ||
52787ef | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-03T23:44 CET (comp) |
Found 20 witnesses for program sv-benchmarks/c/product-lines/elevator_spec2_product09_true-unreach-call_true-termination.cil.c, abcc9b31d7d764cbd1d5e771eb5ec7db4c91cf0b5a8ad87f4976c474bc7b816a
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/abcc9b31d7d764cbd1d5e771eb5ec7db4c91cf0b5a8ad87f4976c474bc7b816a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
96db9d4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T02:04 CET (sv-comp) | ||
a42f683 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T07:36:31 | ||
bad21f1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T02:06 CET (sv-comp) | ||
3221483 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7 | 291 | 2018-12-10T18:33:14+01:00 | ||
effa0a7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 300 | 2018-12-07T06:40:07+01:00 | ||
dab97df | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 291 | 2018-12-10T19:57:17+01:00 | 3221483 | |
f748c96 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 291 | 2018-12-10T10:31:53+01:00 | 2c33ebc | |
583ddc4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 291 | 2018-12-08T23:17:11+01:00 | 96db9d4 | |
f518712 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 291 | 2018-12-08T21:44:58+01:00 | a42f683 | |
f0ee82a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 297 | 2018-12-08T06:15:59+01:00 | effa0a7 | |
58dc716 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 291 | 2018-12-08T04:23:52+01:00 | 4b6bce1 | |
25254d4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 291 | 2018-12-08T02:53:56+01:00 | 2c33ebc | |
9804873 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 291 | 2018-12-07T16:39:14+01:00 | bad21f1 | |
8b119fc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 291 | 2018-12-06T09:28:55+01:00 | 3d162cb | |
ba03603 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 291 | 2018-12-06T09:09:52+01:00 | 913acd9 | |
ebb29cf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 291 | 2018-12-06T08:08:28+01:00 | 26c30d5 | |
4ea8e42 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 291 | 2018-12-06T07:59:40+01:00 | ea2a6bb | |
913acd9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 291 | 2018-12-05T12:58:01+01:00 | ||
17a2f87 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T00:06 CET (sv-comp) | ||
2d974de | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-06T23:32 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec2_product09_true-unreach-call_true-termination.cil.c, abcc9b31d7d764cbd1d5e771eb5ec7db4c91cf0b5a8ad87f4976c474bc7b816a
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/abcc9b31d7d764cbd1d5e771eb5ec7db4c91cf0b5a8ad87f4976c474bc7b816a.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_product09_true-unreach-call_true-termination.cil.c, abcc9b31d7d764cbd1d5e771eb5ec7db4c91cf0b5a8ad87f4976c474bc7b816a
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/abcc9b31d7d764cbd1d5e771eb5ec7db4c91cf0b5a8ad87f4976c474bc7b816a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |