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/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i |
programSHA | d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8 |
witnessName | results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i.files/witness.graphml |
witnessSHA | 2ca7eefaa2fb54bbbf76c4bcab0a08bb120d3a3543dc55f58f562775cb7ffa38 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-02T05:44 CET (sv-comp) |
producer | Symbiotic |
program-sha256 | d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_9febffd2-4ddc-4277-b3b4-e505eebfdb95/sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i |
programhash | 10cc4caffca660fca2e6a4a0cd5f7ba7ba4e10af |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/2ca7eefaa2fb54bbbf76c4bcab0a08bb120d3a3543dc55f58f562775cb7ffa38.graphml |
witness-sha256 | 2ca7eefaa2fb54bbbf76c4bcab0a08bb120d3a3543dc55f58f562775cb7ffa38 |
witness-size | 784 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i, d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i, d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i, d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i, d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i, d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i, d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 34 witnesses for program sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i, d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3db7b4f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 23 | 2017-12-03T05:17Z | ||
2ca7eef | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T05:44 CET (sv-comp) | ||
b3c4137 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Map2Check | 5 | 2017-12-01T21:00 CET (sv-comp) | ||
9d3f137 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 24 | 2017-12-02T02:30Z | ||
48ba2d8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T22:22:31.422790 | ||
9053f36 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T08:40:29.084997 | ||
8ad6ed1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T03:02:45.795493 | ||
302efbe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T08:36:39.191314 | ||
95706b3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 77 | 2017-12-01T17:40 CET (sv-comp) | ||
1d64ad7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 15 | 2017-12-03T03:19:47+01:00 | ||
aa4d670 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-01T05:07:23+01:00 | ||
fe60d3f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-03T06:51:29+01:00 | 114d676 | |
a16fffe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 14 | 2017-12-03T04:19:36+01:00 | 2294215 | |
2a43ff8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-03T01:56:40+01:00 | 2d93330 | |
8a21fe7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-03T00:52:34+01:00 | 9acf203 | |
d05bf39 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-02T19:53:56+01:00 | d281c1e | |
2e35a6e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-02T15:28:33+01:00 | f6d1cac | |
bcfcba1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-02T08:58:54+01:00 | 9f05720 | |
72d153f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-01T22:21:39+01:00 | 487eb9d | |
971db9d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-01T22:04:46+01:00 | 257c0f6 | |
3811cce | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-01T08:13:34+01:00 | 2fbd5d7 | |
f33d1fa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-01T06:20:53+01:00 | d0616d6 | |
e92fa20 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-01T05:45:12+01:00 | d13112e | |
e30005e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 14 | 2017-12-01T05:42:41+01:00 | b30f955 | |
558563b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-01T05:08:51+01:00 | 8caace8 | |
21b1c9a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-12-01T05:00:49+01:00 | ea52582 | |
6418ae3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 13 | 2017-11-30T15:11:11+01:00 | ||
40c6516 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 18 | 2017-11-30T17:13:50+01:00 | ||
903c7df | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 14 | 2017-11-30T11:53:25+01:00 | ||
0c7c179 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 13 | 2017-12-01T22:22:33+01:00 | ||
d887739 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 255 | 2017-11-30T17:15 CET (sv-comp) | ||
3b45f89 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 23 | 2017-12-02T02:59Z | ||
183a8c5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 29 | 2017-11-30T20:38 CET (sv-comp) | ||
e08dba0 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 252 | 2017-12-01T15:24 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i, d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/d74b9ea066fb7f17f4f9b2b3a94a770c4bbb7e4584e29ffac6eb4606412daaf8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |