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/array_false-unreach-call_true-termination.i |
programSHA | 1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340 |
witnessName | results-verified/ukojak.2018-12-08_1104.logfiles/sv-comp19_prop-reachsafety.array_false-unreach-call_true-termination.i.files/witness.graphml |
witnessSHA | 034b255e0154aff961fb2d45b3a4d57593a42ce285d6ae91f86c6910a4f48368 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-09T00:38Z |
producer | Kojak |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_191ef576-0f29-4451-83cb-b98b5a529add/sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i |
programhash | c9c01a6cc6331754f7a6c99ec20becb53bf53c79 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/034b255e0154aff961fb2d45b3a4d57593a42ce285d6ae91f86c6910a4f48368.graphml |
witness-sha256 | 034b255e0154aff961fb2d45b3a4d57593a42ce285d6ae91f86c6910a4f48368 |
witness-size | 6982 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i, 1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i, 1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i, 1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i, 1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i, 1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 26 witnesses for program sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i, 1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
bf0f32e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T05:23 CET (sv-comp) | ||
49fa837 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 4 | 2018-12-08T06:39:30 | ||
1a32c83 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 6 | 2018-12-06T23:23 CET (sv-comp) | ||
33fe5fe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 8 | 2018-12-08T04:22:40+01:00 | ||
9397997 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-10T20:37:31+01:00 | ff4ec5a | |
eb6fdd5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-09T21:23:33+01:00 | c703a73 | |
95bdcee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-09T20:53:07+01:00 | d34f3fe | |
0d08d06 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-09T20:38:41+01:00 | cb9e3b2 | |
cfa43ad | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-09T20:28:02+01:00 | 034b255 | |
7807c7d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-09T18:20:23+01:00 | 725166b | |
27d0d5b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T23:43:49+01:00 | bf0f32e | |
c6ea9bc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T22:08:36+01:00 | 49fa837 | |
6319678 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T09:05:31+01:00 | 33fe5fe | |
e7f6ef3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T05:03:38+01:00 | 6a64cbc | |
c30f332 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T03:56:46+01:00 | 62e95e2 | |
4b65d25 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-07T18:48:09+01:00 | b06206e | |
542dda3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-07T17:43:20+01:00 | 1a32c83 | |
31203d6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-07T01:17:53+01:00 | 0fb324c | |
0eaae8d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T10:19:04+01:00 | 92c1737 | |
56cae41 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T09:47:56+01:00 | 8d222a7 | |
35d6d4a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T09:42:46+01:00 | d969a83 | |
09acbe2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T09:11:09+01:00 | 8d4f420 | |
8d222a7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T00:46:31+01:00 | ||
df1d21d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:16:50+01:00 | 618d552 | |
6cde6d3 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T08:25 CET (sv-comp) | ||
0317284 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T05:37 CET (sv-comp) |
Found 22 witnesses for program sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i, 1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c674f89 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | skink | 3 | 2017-12-01T22:13 CET (sv-comp) | ||
6e014ee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | VeriAbs 1.3 | 6 | Sat Dec 2 23:41:57 2017 | ||
49067f8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 7 | 2017-12-03T02:25Z | ||
0d8f68f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T04:25 CET (sv-comp) | ||
f66d2df | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 7 | 2017-12-02T12:51Z | ||
8111e03 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-01T22:14:40.520160 | ||
f30467e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T19:40:20.043908 | ||
c25d788 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 5 | 2017-12-01T18:58 CET (sv-comp) | ||
0b7fc17 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 5 | 2017-11-30T19:27 CET (sv-comp) | ||
7305bd9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-11-30T14:19:49+01:00 | ||
32b7524 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 12 | 2017-11-30T19:21:18+01:00 | ||
e104ed2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 6 | 2017-12-01T01:29:53+01:00 | ||
c4f66fc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 7 | 2017-12-02T02:57:30+01:00 | ||
e6fde29 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 6 | 2017-12-01T00:33 CET (sv-comp) | ||
7b220db | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 7 | 2017-12-02T03:56Z | ||
ba97187 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 6 | 2017-11-30T13:17 CET (sv-comp) | ||
cf2607d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Map2Check | 3 | 2017-12-01T21:46 CET (sv-comp) | ||
4c79683 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T02:04:59.626130 | ||
aaa77eb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T08:42:57.060272 | ||
d4de1bc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-01T22:36:55+01:00 | 1009665 | |
bd79bdb | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 6 | 2017-12-01T16:24 CET (sv-comp) | ||
a4d731d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 11 | 2017-12-01T12:26 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/loops/array_false-unreach-call_true-termination.i, 1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/1c5e596b68cc4c397dc855ccc6dc2fb4467f6a56696cb2be3056f7eb683c9340.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |