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).
Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i, aae036351aa72f77b37d8213a1f21936aa19a00887d2755ffa88e814c3e58cac
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/aae036351aa72f77b37d8213a1f21936aa19a00887d2755ffa88e814c3e58cac.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_all_false-unreach-call_true-valid-memsafety.i, aae036351aa72f77b37d8213a1f21936aa19a00887d2755ffa88e814c3e58cac
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/aae036351aa72f77b37d8213a1f21936aa19a00887d2755ffa88e814c3e58cac.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_all_false-unreach-call_true-valid-memsafety.i, aae036351aa72f77b37d8213a1f21936aa19a00887d2755ffa88e814c3e58cac
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/aae036351aa72f77b37d8213a1f21936aa19a00887d2755ffa88e814c3e58cac.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_all_false-unreach-call_true-valid-memsafety.i, aae036351aa72f77b37d8213a1f21936aa19a00887d2755ffa88e814c3e58cac
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/aae036351aa72f77b37d8213a1f21936aa19a00887d2755ffa88e814c3e58cac.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 16 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i, aae036351aa72f77b37d8213a1f21936aa19a00887d2755ffa88e814c3e58cac
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/aae036351aa72f77b37d8213a1f21936aa19a00887d2755ffa88e814c3e58cac.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
798f86d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 133 | 2019-11-30T00:58:59+01:00 | ||
9ba884b | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 133 | 2019-12-01T05:55:49+01:00 | ||
674c211 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-01 11:03:40 | ||
40872bb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 15 | 2019-12-04T00:36 CET (comp) | ||
0fce5e1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 22 | 2019-12-11T22:00:46+01:00 | ea8e215 | |
2d2fb97 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 22 | 2019-12-11T21:09:43+01:00 | 674c211 | |
e1d492a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 22 | 2019-12-11T20:56:48+01:00 | d1e5ba6 | |
8cc2f28 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 22 | 2019-12-11T20:44:33+01:00 | 123a95f | |
74dcf69 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 22 | 2019-12-08T00:07:41+01:00 | 81e5806 | |
5d31afe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 22 | 2019-12-06T02:40:52+01:00 | 42dc37e | |
a6814f1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 22 | 2019-12-04T02:58:08+01:00 | 40872bb | |
ad2218a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 22 | 2019-12-03T08:57:13+01:00 | 0761f3b | |
4fe8f85 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 22 | 2019-12-03T08:10:13+01:00 | 00db857 | |
00db857 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 26 | 2019-11-30T14:47:19+01:00 | ||
ea8e215 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 21 | 2019-12-01T10:14:34+01:00 | ||
afcb543 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 134 | 2019-12-05T20:21:21+01:00 | a02ffe0 |
Found 19 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i, aae036351aa72f77b37d8213a1f21936aa19a00887d2755ffa88e814c3e58cac
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/aae036351aa72f77b37d8213a1f21936aa19a00887d2755ffa88e814c3e58cac.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7e38b70 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T08:05 CET (sv-comp) | ||
d6d48e0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 133 | 2018-12-05T18:46:20+01:00 | ||
b1255fb | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 133 | 2018-12-08T02:28:57+01:00 | ||
5a3b380 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T07:55 CET (sv-comp) | ||
c0a0493 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 4 | 2018-12-08T11:26:10 | ||
f5c61a3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 17 | 2018-12-07T02:55 CET (sv-comp) | ||
c89f39c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 27 | 2018-12-06T23:15:43+01:00 | ||
c5a5591 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-10T10:48:54+01:00 | c64f5d5 | |
127a515 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-09T18:20:39+01:00 | b9cc05c | |
71b7a22 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-08T23:44:06+01:00 | 5a3b380 | |
4701eec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-08T22:11:41+01:00 | c0a0493 | |
7556774 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-08T07:51:22+01:00 | c89f39c | |
412c7f4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-08T05:03:12+01:00 | 244d89a | |
2c6ebe3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-07T17:44:22+01:00 | f5c61a3 | |
b840b6c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-07T09:18:46+01:00 | 8d7bf35 | |
3f30129 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-06T10:09:23+01:00 | be22940 | |
7931698 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-06T09:48:14+01:00 | 7ccb768 | |
7ccb768 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 27 | 2018-12-06T01:52:51+01:00 | ||
7cd6b15 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 134 | 2018-12-06T09:20:00+01:00 | fea5578 |
Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i, aae036351aa72f77b37d8213a1f21936aa19a00887d2755ffa88e814c3e58cac
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/aae036351aa72f77b37d8213a1f21936aa19a00887d2755ffa88e814c3e58cac.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_all_false-unreach-call_true-valid-memsafety.i, aae036351aa72f77b37d8213a1f21936aa19a00887d2755ffa88e814c3e58cac
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/aae036351aa72f77b37d8213a1f21936aa19a00887d2755ffa88e814c3e58cac.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |