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/ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i |
programSHA | ebd1ec1764021eee55b542e41204dc0aa45e23c6a03b93f6077378f532828b49 |
witnessName | results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-memsafety.ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i.files/witness.graphml |
witnessSHA | 8b97f04a44da01909e77f3b5d21407a27970a471e4f64c33321be129c8c3cf4f |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-06T06:34:11.053810 |
producer | DepthK v3.0 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_a6fac082-b8d2-4a4d-818c-3ed715ee077f/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i |
programhash | e2575629a0892fb5449add5936286efb588d4cc5 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
witness-file | witnessFileByHash/8b97f04a44da01909e77f3b5d21407a27970a471e4f64c33321be129c8c3cf4f.graphml |
witness-sha256 | 8b97f04a44da01909e77f3b5d21407a27970a471e4f64c33321be129c8c3cf4f |
witness-size | 5938 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i, ebd1ec1764021eee55b542e41204dc0aa45e23c6a03b93f6077378f532828b49
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ebd1ec1764021eee55b542e41204dc0aa45e23c6a03b93f6077378f532828b49.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i, ebd1ec1764021eee55b542e41204dc0aa45e23c6a03b93f6077378f532828b49
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ebd1ec1764021eee55b542e41204dc0aa45e23c6a03b93f6077378f532828b49.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i, ebd1ec1764021eee55b542e41204dc0aa45e23c6a03b93f6077378f532828b49
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ebd1ec1764021eee55b542e41204dc0aa45e23c6a03b93f6077378f532828b49.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i, ebd1ec1764021eee55b542e41204dc0aa45e23c6a03b93f6077378f532828b49
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ebd1ec1764021eee55b542e41204dc0aa45e23c6a03b93f6077378f532828b49.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 19 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i, ebd1ec1764021eee55b542e41204dc0aa45e23c6a03b93f6077378f532828b49
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ebd1ec1764021eee55b542e41204dc0aa45e23c6a03b93f6077378f532828b49.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b8814a2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-01 11:37:07 | ||
f95ca3e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 40 | 2019-12-11T21:09:22+01:00 | b8814a2 | |
3c79a60 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 37 | 2019-11-30T21:19:03+01:00 | ||
488c514 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 119 | 2019-12-11T20:54:54+01:00 | 8a2b5ce | |
11a1f73 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 40 | 2019-12-03T08:09:16+01:00 | 0c6cfe1 | |
9a0a04b | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 119 | 2019-12-08T00:06:56+01:00 | 81aff75 | |
a4e6b46 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 40 | 2019-12-11T21:48:36+01:00 | 3c79a60 | |
0c6cfe1 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 37 | 2019-11-29T19:22:58+01:00 | ||
994bdca | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.9 | 119 | 2019-12-05T20:20:15+01:00 | ab89883 | |
aa1eef5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 118 | 2019-12-11T20:28:24+01:00 | 66d225e | |
75bf977 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 118 | 2019-12-11T20:23:34+01:00 | c5f3c49 | |
d7c968f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 118 | 2019-12-11T20:07:50+01:00 | 0b8da93 | |
3855103 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 118 | 2019-12-11T20:02:29+01:00 | ac19487 | |
99618c4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 118 | 2019-12-07T23:40:57+01:00 | a66bf65 | |
9cfb0cc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 118 | 2019-12-07T19:42:41+01:00 | 3e47c21 | |
0f69ce6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 118 | 2019-12-06T01:49:52+01:00 | d386dfc | |
6bd23c0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 118 | 2019-11-30T16:28:36+01:00 | 643c368 | |
643c368 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 118 | 2019-11-29T20:48:10+01:00 | ||
0b8da93 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 118 | 2019-12-01T02:23:24+01:00 |
Found 26 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i, ebd1ec1764021eee55b542e41204dc0aa45e23c6a03b93f6077378f532828b49
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ebd1ec1764021eee55b542e41204dc0aa45e23c6a03b93f6077378f532828b49.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9588687 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T01:03 CET (sv-comp) | ||
96c488d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 41 | 2018-12-07T03:59:53+01:00 | ||
2033a71 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 38 | 2018-12-08T09:02:10+01:00 | 96c488d | |
9d44ada | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 41 | 2018-12-06T06:33:18+01:00 | ||
f7c53a7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 119 | 2018-12-06T09:14:36+01:00 | 81fd00a | |
cba27b4 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 119 | 2018-12-07T09:13:55+01:00 | ff5b3a0 | |
f14b5dd | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 119 | 2018-12-06T10:13:25+01:00 | 8b97f04 | |
6993049 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 37 | 2018-12-08T23:44:53+01:00 | 9588687 | |
5dd11c8 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 37 | 2018-12-07T01:06:59+01:00 | f70d6cc | |
ea59b56 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 38 | 2018-12-06T09:49:14+01:00 | 9d44ada | |
a0fa84b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 119 | 2018-12-08T04:56:49+01:00 | f255854 | |
9f9b920 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T03:15 CET (sv-comp) | ||
48f60f5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T12:16:01 | ||
bc041af | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 118 | 2018-12-07T19:28:04+01:00 | ||
e726235 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-10T20:16:48+01:00 | 9d712e2 | |
26bef30 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-09T20:27:17+01:00 | 50316de | |
21eb5c3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-09T20:04:39+01:00 | e3ae3c0 | |
280ca92 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-09T19:58:25+01:00 | 8d85136 | |
5a8ae63 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-08T23:11:59+01:00 | 9f9b920 | |
bda09fd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-08T21:44:46+01:00 | 48f60f5 | |
5f3b504 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-08T06:21:46+01:00 | bc041af | |
3ccd59b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-08T03:41:44+01:00 | 85e7aad | |
933b955 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-07T17:45:35+01:00 | 1c51905 | |
e7eb087 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-06T09:28:26+01:00 | fb22cb5 | |
1f216fc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-06T08:45:35+01:00 | 9212d40 | |
9212d40 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-05T07:06:01+01:00 |
Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i, ebd1ec1764021eee55b542e41204dc0aa45e23c6a03b93f6077378f532828b49
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ebd1ec1764021eee55b542e41204dc0aa45e23c6a03b93f6077378f532828b49.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i, ebd1ec1764021eee55b542e41204dc0aa45e23c6a03b93f6077378f532828b49
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ebd1ec1764021eee55b542e41204dc0aa45e23c6a03b93f6077378f532828b49.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |