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/ldv-regression/stateful_check_false-unreach-call_false-termination.i |
programSHA | 73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814 |
witnessName | results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.stateful_check_false-unreach-call_false-termination.i.files/witness.graphml |
witnessSHA | 7f2b86018055630268229eb8deb6ea0e691d7ea99bb90c728759acd6f46eff89 |
Key | Value |
architecture | 32bit |
creationtime | 2017-11-30T15:31:18+01:00 |
producer | CPAchecker 1.6.1-svn 26758M |
program-sha256 | 73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814 |
programfile | ../../sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i |
programhash | 1225f82562543767c482452e9133e4a69d5dae70 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/7f2b86018055630268229eb8deb6ea0e691d7ea99bb90c728759acd6f46eff89.graphml |
witness-sha256 | 7f2b86018055630268229eb8deb6ea0e691d7ea99bb90c728759acd6f46eff89 |
witness-size | 29155 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i, 73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i, 73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i, 73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i, 73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 22 witnesses for program sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i, 73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1e7eac2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 3 | 2019-12-01 22:11:10 | ||
9485724 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 13 | 2019-12-03T22:06 CET (comp) | ||
6d73d68 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 24 | 2019-12-11T21:58:29+01:00 | dc78271 | |
17f23e6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 24 | 2019-12-11T21:43:46+01:00 | 4175197 | |
be46c77 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 24 | 2019-12-11T21:09:02+01:00 | 1e7eac2 | |
f93905d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 27 | 2019-12-11T20:54:20+01:00 | 1a20482 | |
3981322 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 130 | 2019-12-11T20:44:27+01:00 | 1229218 | |
dc7655f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 24 | 2019-12-08T01:51:16+01:00 | 058dc0c | |
18186f2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 24 | 2019-12-08T00:26:02+01:00 | d901158 | |
2f1ed96 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 24 | 2019-12-07T21:15:57+01:00 | 0a75916 | |
91db1d7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 24 | 2019-12-04T02:58:17+01:00 | 9485724 | |
28d4c51 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 24 | 2019-12-03T08:57:15+01:00 | fb3b5c4 | |
59c2aa0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 24 | 2019-12-03T08:10:33+01:00 | a2c894c | |
a2c894c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 21 | 2019-11-30T13:34:22+01:00 | ||
058dc0c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 24 | 2019-12-07T21:07:16+01:00 | ||
dc78271 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 24 | 2019-12-01T00:30:32+01:00 | ||
ce8d36c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-12-08T00:06:06+01:00 | 6499501 | |
ea6849a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-12-05T20:20:14+01:00 | 7658021 | |
ece3e27 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-12-05T19:34:11+01:00 | 678d5c7 | |
b12d9ba | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Symbiotic | 1 | 2019-12-01 12:04:04 | ||
f88bf91 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 21 | 2019-11-30T12:01:03+01:00 | ||
b0eb35c | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 21 | 2019-12-01T17:44:05+01:00 |
Found 26 witnesses for program sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i, 73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c4763f8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T12:41 CET (sv-comp) | ||
b64c56d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 5 | 2018-12-07T21:39:20 | ||
8b28bab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 24 | 2018-12-10T17:39:42+01:00 | ||
d0e5e2d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 21 | 2018-12-07T13:20:21+01:00 | ||
9669893 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 24 | 2018-12-10T20:36:27+01:00 | 8b28bab | |
5994aaa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 24 | 2018-12-10T10:48:41+01:00 | fa028b7 | |
adec096 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 24 | 2018-12-09T20:53:08+01:00 | e1f0ebe | |
b56a32f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 24 | 2018-12-09T20:38:58+01:00 | 58d0cf0 | |
6b14042 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 24 | 2018-12-09T20:23:20+01:00 | 91f7f9c | |
fd3a268 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 430 | 2018-12-09T18:20:44+01:00 | 363fe06 | |
6a65ffa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 24 | 2018-12-08T23:44:03+01:00 | c4763f8 | |
4b01c06 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 46 | 2018-12-08T22:10:23+01:00 | b64c56d | |
6a7316a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 24 | 2018-12-08T07:45:38+01:00 | d0e5e2d | |
7fb0b24 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 24 | 2018-12-08T05:03:20+01:00 | 499b3f3 | |
ee64a17 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 24 | 2018-12-08T04:36:53+01:00 | fa028b7 | |
570355f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 24 | 2018-12-06T10:19:21+01:00 | 61d3bbe | |
94cc15c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 24 | 2018-12-06T09:49:11+01:00 | c0dc24e | |
ea9678e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 75 | 2018-12-06T09:09:34+01:00 | cc88790 | |
c0dc24e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 21 | 2018-12-06T05:44:31+01:00 | ||
4f747d7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 19 | 2018-12-07T09:20:32+01:00 | b067243 | |
bd61638 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 19 | 2018-12-06T09:40:29+01:00 | abe9bc0 | |
3accc8a | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 21 | 2018-12-06T23:59:08+01:00 | ||
504cad4 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 21 | 2018-12-09T20:33:23+01:00 | ||
b90c2c2 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-06T10:18:45+01:00 | ||
716f039 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-06T09:40:28+01:00 | ||
0dd4d13 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 21 | 2018-12-06T01:03:45+01:00 |
Found 19 witnesses for program sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i, 73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9b76c74 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 21 | 2017-12-03T04:31Z | ||
c8562bf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T09:30 CET (sv-comp) | ||
b067243 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | PredatorHP | 5 | 2017-12-01T20:41 CET (sv-comp) | ||
49df642 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 21 | 2017-12-02T05:15Z | ||
321c75c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T00:07:47.254772 | ||
aa88f22 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T13:08:45.584878 | ||
268d30f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 6 | 2017-12-01T20:28 CET (sv-comp) | ||
e1a0191 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 6 | 2017-11-30T22:58 CET (sv-comp) | ||
828316d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn | 29 | 2017-12-03T01:06:14+01:00 | ||
97451d6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 21 | 2017-11-30T15:35:28+01:00 | ||
7f2b860 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 29 | 2017-11-30T15:31:18+01:00 | ||
7346899 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 18 | 2017-12-01T00:29:48+01:00 | ||
d15c9e5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 21 | 2017-12-01T21:48:53+01:00 | ||
9238361 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 17 | 2017-12-01T02:21 CET (sv-comp) | ||
ae3edb2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 21 | 2017-12-02T02:30Z | ||
0cce2dd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 9 | 2017-11-30T23:18 CET (sv-comp) | ||
cb7abd3 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 21 | 2017-12-01T18:17:46+01:00 | ||
cf4ed9a | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 7 | 2017-12-03T11:15Z | ||
da6d59b | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 4 | 2017-12-01T12:51 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-regression/stateful_check_false-unreach-call_false-termination.i, 73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/73f7c589ad229d43e506c75df523afaf57cb0d2041473b76ec8812caa952a814.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |