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/eca-rers2012/Problem01_label37_false-unreach-call_false-termination.c |
programSHA | 9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994 |
witnessName | results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.Problem01_label37_false-unreach-call_false-termination.c.files/witness.graphml |
witnessSHA | 0dd5c1396733efea143ea325068f6e56ff03c110e4b243ee1e88db25cbd2be15 |
Key | Value |
architecture | 32bit |
creationtime | 2017-11-30T16:01:52+01:00 |
producer | CPAchecker 1.6.1-svn 26725 |
program-sha256 | 9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994 |
programfile | ../../sv-benchmarks/c/eca-rers2012/Problem01_label37_false-unreach-call_false-termination.c |
programhash | fa966b8d35f41797c67ed2115fa88ccdba9ca513 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/0dd5c1396733efea143ea325068f6e56ff03c110e4b243ee1e88db25cbd2be15.graphml |
witness-sha256 | 0dd5c1396733efea143ea325068f6e56ff03c110e4b243ee1e88db25cbd2be15 |
witness-size | 112206 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label37_false-unreach-call_false-termination.c, 9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label37_false-unreach-call_false-termination.c, 9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label37_false-unreach-call_false-termination.c, 9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label37_false-unreach-call_false-termination.c, 9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 18 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label37_false-unreach-call_false-termination.c, 9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e896319 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 2 | 2019-12-02 05:04:22 | ||
f7e338b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 69 | 2019-12-03T22:18 CET (comp) | ||
81fbabe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 204 | 2019-12-11T21:45:37+01:00 | a86cf6c | |
2008791 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 203 | 2019-12-11T21:09:35+01:00 | e896319 | |
a3272ab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 204 | 2019-12-11T20:55:08+01:00 | db6647b | |
d5bea90 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 204 | 2019-12-11T20:44:49+01:00 | a5f5765 | |
51a4ce5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 205 | 2019-12-08T01:51:25+01:00 | 9c5c7cc | |
ad97aff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 257 | 2019-12-04T02:58:30+01:00 | f7e338b | |
52511ee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 204 | 2019-12-03T08:09:46+01:00 | 4cbd708 | |
4cbd708 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 202 | 2019-11-30T03:25:29+01:00 | ||
a86cf6c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 203 | 2019-12-01T16:50:53+01:00 | ||
9b69c27 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-11T21:52:32+01:00 | ddd18ed | |
7dc0acb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-08T00:27:15+01:00 | ea9a66e | |
b829193 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-07T21:15:01+01:00 | 9a9afb7 | |
056ffea | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-05T20:21:35+01:00 | 659beba | |
5e92688 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 287 | 2019-12-05T19:35:09+01:00 | 45f97b1 | |
04ea9d1 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 339 | 2019-11-30T06:51:00+01:00 | ||
2fc6156 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 339 | 2019-12-01T12:44:54+01:00 |
Found 23 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label37_false-unreach-call_false-termination.c, 9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
173e408 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T01:25 CET (sv-comp) | ||
2b9eda2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 10 | 2018-12-08T07:15:43 | ||
7ff2042 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 80 | 2018-12-07T12:12 CET (sv-comp) | ||
190cdb1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 203 | 2018-12-07T21:55:14+01:00 | ||
3c4da55 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 205 | 2018-12-10T20:36:27+01:00 | da32c0a | |
c221c0d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 204 | 2018-12-09T18:21:54+01:00 | f778ba1 | |
5bed680 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 207 | 2018-12-08T23:44:40+01:00 | 173e408 | |
e78a83d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 204 | 2018-12-08T22:10:15+01:00 | 2b9eda2 | |
5bb341e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 204 | 2018-12-08T08:58:18+01:00 | 190cdb1 | |
4b94c76 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 203 | 2018-12-08T05:06:36+01:00 | c40b651 | |
57a2065 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 257 | 2018-12-07T17:43:57+01:00 | 7ff2042 | |
59747df | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 204 | 2018-12-06T10:20:05+01:00 | 24f0724 | |
80b906c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 204 | 2018-12-06T09:48:49+01:00 | 2c93a9c | |
bc99b00 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 257 | 2018-12-06T09:13:59+01:00 | f683275 | |
2c93a9c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 202 | 2018-12-05T12:28:10+01:00 | ||
93f16d0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-09T20:53:39+01:00 | 65a87a7 | |
3d27876 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-09T20:36:52+01:00 | 082fd93 | |
d711952 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-09T20:33:32+01:00 | cd507e1 | |
961edc1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 287 | 2018-12-06T09:42:02+01:00 | d6e9ddb | |
ef6ad8a | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 339 | 2018-12-07T19:03:11+01:00 | ||
169e7c3 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 336 | 2018-12-08T07:59:24+01:00 | ||
ad24eaf | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 324 | 2018-12-06T09:49:07+01:00 | ||
fe94585 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 327 | 2018-12-06T00:04:59+01:00 |
Found 15 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label37_false-unreach-call_false-termination.c, 9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7a422b6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Veriabs | 3 | 2017-12-02T20:18 CET (sv-comp) | ||
ca42a29 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T00:04 CET (sv-comp) | ||
39b74cb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 176 | 2017-12-02T10:46Z | ||
1ff57d7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 5 | 2017-12-01T22:43:04.703813 | ||
9d53063 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 5 | 2017-12-01T08:25:56.869698 | ||
89ed45d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 14 | 2017-12-01T15:54 CET (sv-comp) | ||
809d0a7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 14 | 2017-12-01T04:41 CET (sv-comp) | ||
5f2f453 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 117 | 2017-11-30T15:52:21+01:00 | ||
e8c96d2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 300 | 2017-11-30T14:21:48+01:00 | ||
0dd5c13 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 112 | 2017-11-30T16:01:52+01:00 | ||
5220894 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 182 | 2017-12-02T00:29:39+01:00 | ||
1a8f74d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 88 | 2017-11-30T22:16 CET (sv-comp) | ||
69317e7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 176 | 2017-12-02T06:11Z | ||
81513a5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 89 | 2017-11-30T20:11 CET (sv-comp) | ||
9a66756 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 31 | 2017-12-01T16:51 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label37_false-unreach-call_false-termination.c, 9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/9e265356835a15b812a26e71cb09dac513a37c44ada4e109cd931128b9489994.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |