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/sum03_false-unreach-call_true-termination.i |
programSHA | 2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0 |
witnessName | results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-reachsafety.sum03_false-unreach-call_true-termination.i.files/witness.graphml |
witnessSHA | bc6b27ba91816f26f479dc629551b159bf38c596198839fc0ec22908109c4876 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-05T12:37:21.549628 |
producer | DepthK v3.0 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_b5f31d20-7df0-4795-a939-ddec44692b65/sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i |
programhash | a5bec83c84f47b7653d49cdbe6bc7857a2bc0080 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/bc6b27ba91816f26f479dc629551b159bf38c596198839fc0ec22908109c4876.graphml |
witness-sha256 | bc6b27ba91816f26f479dc629551b159bf38c596198839fc0ec22908109c4876 |
witness-size | 3671 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i, 2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i, 2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i, 2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i, 2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 20 witnesses for program sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i, 2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
68e9b8e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-01 13:26:07 | ||
84f8fcd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 18 | 2019-12-04T00:19 CET (comp) | ||
a175e4e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | GACAL | 25 | 2019-12-07T23:20 CET (comp) | ||
19c449e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 39 | 2019-12-11T21:55:09+01:00 | f7d70fa | |
81ed9bd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 39 | 2019-12-11T21:09:20+01:00 | 68e9b8e | |
e129ecb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 39 | 2019-12-11T20:55:22+01:00 | 3385778 | |
208c7c6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 39 | 2019-12-11T20:44:29+01:00 | 55afb67 | |
818d693 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 39 | 2019-12-08T01:51:58+01:00 | 089fccc | |
073dd36 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 39 | 2019-12-08T00:26:17+01:00 | ec57e86 | |
16d6cbf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 39 | 2019-12-04T02:58:18+01:00 | 84f8fcd | |
39bff85 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 39 | 2019-12-03T08:56:47+01:00 | 34af031 | |
d57287e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 39 | 2019-12-03T08:09:45+01:00 | 4801456 | |
4801456 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 38 | 2019-11-30T00:38:44+01:00 | ||
089fccc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 39 | 2019-12-07T13:26:54+01:00 | ||
f7d70fa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 38 | 2019-12-01T15:51:54+01:00 | ||
dd6ffa4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-08T00:14:01+01:00 | a175e4e | |
df8a879 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-06T02:41:07+01:00 | 7635cb4 | |
6be96cf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-05T20:20:58+01:00 | 9f2fdda | |
408d310 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-05T19:34:01+01:00 | ffb2aa6 | |
d2b28a4 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:42 CET (comp) |
Found 27 witnesses for program sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i, 2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f351483 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 2 | 2018-12-08T07:38 CET (sv-comp) | ||
7431f19 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 9 | 2018-12-08T02:52:12 | ||
e6606c4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 21 | 2018-12-07T03:57 CET (sv-comp) | ||
97923ff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 37 | 2018-12-10T17:09:30+01:00 | ||
a3411fa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 38 | 2018-12-07T18:17:33+01:00 | ||
e98aff9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 39 | 2018-12-10T20:36:20+01:00 | 97923ff | |
4177b00 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 39 | 2018-12-10T10:48:40+01:00 | 0300aa1 | |
9d1f667 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 39 | 2018-12-09T20:53:24+01:00 | 5b27843 | |
397f254 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 39 | 2018-12-09T20:37:03+01:00 | 03177d4 | |
1a5d2bd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 39 | 2018-12-09T20:26:50+01:00 | 054e841 | |
33f4fef | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 39 | 2018-12-09T18:20:25+01:00 | d90656a | |
eabc164 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 39 | 2018-12-08T23:43:47+01:00 | f351483 | |
5aef862 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 39 | 2018-12-08T22:11:17+01:00 | 7431f19 | |
4d03b08 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 39 | 2018-12-08T07:51:04+01:00 | a3411fa | |
ba8ba2c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 39 | 2018-12-08T05:04:42+01:00 | f9db73d | |
5afcb8e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 39 | 2018-12-08T03:38:40+01:00 | 0300aa1 | |
9f0066f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 39 | 2018-12-07T18:12:29+01:00 | 39f2e79 | |
c3fcdb1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 39 | 2018-12-07T17:45:27+01:00 | e6606c4 | |
b0aa6b1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 39 | 2018-12-06T10:18:45+01:00 | bc6b27b | |
15cdd3f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 39 | 2018-12-06T09:48:26+01:00 | 71410e6 | |
44f6532 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 39 | 2018-12-06T09:15:43+01:00 | f611c89 | |
71410e6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 38 | 2018-12-05T13:52:05+01:00 | ||
731c857 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-07T01:08:58+01:00 | 266b1a0 | |
738e2a9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:40:58+01:00 | 084241e | |
b244324 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:18:23+01:00 | cbae9d0 | |
018a082 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T07:00 CET (sv-comp) | ||
5dc5ac0 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T03:18 CET (sv-comp) |
Found 20 witnesses for program sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i, 2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
31a0462 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | skink | 6 | 2017-12-01T22:40 CET (sv-comp) | ||
804399b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 33 | 2017-12-03T05:07Z | ||
b65f8a6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T10:36 CET (sv-comp) | ||
cd0bfe7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Map2Check | 3 | 2017-12-01T20:15 CET (sv-comp) | ||
a0ef6b3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 33 | 2017-12-02T09:56Z | ||
846853e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-01T13:48:49.300259 | ||
eee6972 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T18:15:36.750606 | ||
e886d26 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 11 | 2017-12-01T19:46 CET (sv-comp) | ||
9c1e0bc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 11 | 2017-11-30T16:06 CET (sv-comp) | ||
a6c276c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn | 35 | 2017-12-02T18:41:16+01:00 | ||
f65ad9a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 36 | 2017-12-01T02:05:42+01:00 | ||
f14025e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 39 | 2017-11-30T14:36:03+01:00 | ||
d712fc6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 28 | 2017-12-01T01:28:30+01:00 | ||
ff0f576 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 27 | 2017-12-02T12:36:47+01:00 | ||
b6d93f2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 18 | 2017-11-30T16:05 CET (sv-comp) | ||
e5c75b2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 33 | 2017-12-02T03:10Z | ||
b788374 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 21 | 2017-11-30T20:54 CET (sv-comp) | ||
a495352 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T23:16:37.880094 | ||
f526582 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T14:52:37.254919 | ||
b737687 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 18 | 2017-12-01T18:14 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/loops/sum03_false-unreach-call_true-termination.i, 2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/2a3547b16f75be3d225cb90d16687f3917cbb2360e0681ebeeb6cce258fb5cb0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |