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_product23_true-unreach-call_true-termination.cil.c |
programSHA | 0f3dbf1bcf3c9f2454859eae43758a6b9d5262bcb577ab59c893d04b2fbcb32b |
witnessName | results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.elevator_spec14_product23_true-unreach-call_true-termination.cil.c.files/witness.graphml |
witnessSHA | c25a00995f78f771407ca30e7d6e2954021d0d09418c7a7aa582a15c2314cbd4 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-01T23:07 CET (sv-comp) |
producer | Symbiotic |
program-sha256 | 0f3dbf1bcf3c9f2454859eae43758a6b9d5262bcb577ab59c893d04b2fbcb32b |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_ff641117-89d4-4a74-9068-f340d92256c6/sv-benchmarks/c/product-lines/elevator_spec14_product23_true-unreach-call_true-termination.cil.c |
programhash | 7371ebd67ccb7cc615db98d4b0ad2394dcc7361b |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/c25a00995f78f771407ca30e7d6e2954021d0d09418c7a7aa582a15c2314cbd4.graphml |
witness-sha256 | c25a00995f78f771407ca30e7d6e2954021d0d09418c7a7aa582a15c2314cbd4 |
witness-size | 780 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec14_product23_true-unreach-call_true-termination.cil.c, 0f3dbf1bcf3c9f2454859eae43758a6b9d5262bcb577ab59c893d04b2fbcb32b
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/0f3dbf1bcf3c9f2454859eae43758a6b9d5262bcb577ab59c893d04b2fbcb32b.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_product23_true-unreach-call_true-termination.cil.c, 0f3dbf1bcf3c9f2454859eae43758a6b9d5262bcb577ab59c893d04b2fbcb32b
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/0f3dbf1bcf3c9f2454859eae43758a6b9d5262bcb577ab59c893d04b2fbcb32b.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_product23_true-unreach-call_true-termination.cil.c, 0f3dbf1bcf3c9f2454859eae43758a6b9d5262bcb577ab59c893d04b2fbcb32b
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/0f3dbf1bcf3c9f2454859eae43758a6b9d5262bcb577ab59c893d04b2fbcb32b.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_product23_true-unreach-call_true-termination.cil.c, 0f3dbf1bcf3c9f2454859eae43758a6b9d5262bcb577ab59c893d04b2fbcb32b
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/0f3dbf1bcf3c9f2454859eae43758a6b9d5262bcb577ab59c893d04b2fbcb32b.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_product23_true-unreach-call_true-termination.cil.c, 0f3dbf1bcf3c9f2454859eae43758a6b9d5262bcb577ab59c893d04b2fbcb32b
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/0f3dbf1bcf3c9f2454859eae43758a6b9d5262bcb577ab59c893d04b2fbcb32b.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_product23_true-unreach-call_true-termination.cil.c, 0f3dbf1bcf3c9f2454859eae43758a6b9d5262bcb577ab59c893d04b2fbcb32b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/0f3dbf1bcf3c9f2454859eae43758a6b9d5262bcb577ab59c893d04b2fbcb32b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 22 witnesses for program sv-benchmarks/c/product-lines/elevator_spec14_product23_true-unreach-call_true-termination.cil.c, 0f3dbf1bcf3c9f2454859eae43758a6b9d5262bcb577ab59c893d04b2fbcb32b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/0f3dbf1bcf3c9f2454859eae43758a6b9d5262bcb577ab59c893d04b2fbcb32b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c25a009 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-01T23:07 CET (sv-comp) | ||
8593e1f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T02:21:23.761632 | ||
da11697 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T13:53:18.545526 | ||
7e2d210 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T05:32:38.861099 | ||
c060a18 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T11:44:47.329061 | ||
b4babe8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 201 | 2017-12-01T15:25 CET (sv-comp) | ||
608e82c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 296 | 2017-12-03T00:58:53+01:00 | ||
8ef0f5a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-11-30T16:30:57+01:00 | ||
4871e2b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 296 | 2017-12-03T04:30:34+01:00 | 3736de7 | |
7d150d4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 296 | 2017-12-02T20:37:14+01:00 | 13ed8f5 | |
d38630d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 296 | 2017-12-02T07:37:51+01:00 | 02523f6 | |
14b749f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 296 | 2017-12-01T22:27:57+01:00 | 8b176f7 | |
cca769d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 296 | 2017-12-01T08:14:08+01:00 | cafb840 | |
0d62d93 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 296 | 2017-12-01T05:59:28+01:00 | 498cb57 | |
b855269 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 296 | 2017-12-01T05:38:45+01:00 | 161cf3a | |
59fca90 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 296 | 2017-12-01T04:41:02+01:00 | f234788 | |
32a5a43 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 296 | 2017-11-30T14:54:51+01:00 | ||
d5c1fa4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 296 | 2017-11-30T14:46:53+01:00 | ||
0da8199 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 553 | 2017-11-30T11:52 CET (sv-comp) | ||
762d8fc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 14666 | 2017-12-01T02:59 CET (sv-comp) | ||
472d0a2 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 553 | 2017-12-01T15:35 CET (sv-comp) | ||
fccff00 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 14666 | 2017-12-01T14:16 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/product-lines/elevator_spec14_product23_true-unreach-call_true-termination.cil.c, 0f3dbf1bcf3c9f2454859eae43758a6b9d5262bcb577ab59c893d04b2fbcb32b
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/0f3dbf1bcf3c9f2454859eae43758a6b9d5262bcb577ab59c893d04b2fbcb32b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |