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_outl_true-unreach-call_false-valid-memtrack.i |
programSHA | 59c01c002953c422d4be2154bb5e09b5ab70235e1921dc0ea47ecb7a85dad5de |
witnessName | results-verified/skink.2018-12-07_1200.logfiles/sv-comp19_prop-reachsafety.ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i.files/witness.graphml |
witnessSHA | c36441f0881bf03503aeefd2544569a058bc132a01862bd15fab480dbf465d5a |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-07T16:53 CET (sv-comp) |
memorymodel | simple |
producer | skink |
programfile | ../../sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i |
programhash | 4d95ac846195c923ba14460571f07f6424e0aa6b |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/c36441f0881bf03503aeefd2544569a058bc132a01862bd15fab480dbf465d5a.graphml |
witness-sha256 | c36441f0881bf03503aeefd2544569a058bc132a01862bd15fab480dbf465d5a |
witness-size | 2615 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i, 59c01c002953c422d4be2154bb5e09b5ab70235e1921dc0ea47ecb7a85dad5de
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/59c01c002953c422d4be2154bb5e09b5ab70235e1921dc0ea47ecb7a85dad5de.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_outl_true-unreach-call_false-valid-memtrack.i, 59c01c002953c422d4be2154bb5e09b5ab70235e1921dc0ea47ecb7a85dad5de
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/59c01c002953c422d4be2154bb5e09b5ab70235e1921dc0ea47ecb7a85dad5de.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_outl_true-unreach-call_false-valid-memtrack.i, 59c01c002953c422d4be2154bb5e09b5ab70235e1921dc0ea47ecb7a85dad5de
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/59c01c002953c422d4be2154bb5e09b5ab70235e1921dc0ea47ecb7a85dad5de.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_outl_true-unreach-call_false-valid-memtrack.i, 59c01c002953c422d4be2154bb5e09b5ab70235e1921dc0ea47ecb7a85dad5de
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/59c01c002953c422d4be2154bb5e09b5ab70235e1921dc0ea47ecb7a85dad5de.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_outl_true-unreach-call_false-valid-memtrack.i, 59c01c002953c422d4be2154bb5e09b5ab70235e1921dc0ea47ecb7a85dad5de
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/59c01c002953c422d4be2154bb5e09b5ab70235e1921dc0ea47ecb7a85dad5de.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4b919ab | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-02 01:06:39 | ||
3d736a5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 40 | 2019-12-03T08:10:02+01:00 | 0330a57 | |
8d25c82 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 119 | 2019-12-08T00:07:40+01:00 | be06277 | |
aada169 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 119 | 2019-12-05T20:20:29+01:00 | 31d6ef1 | |
d3236cc | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 40 | 2019-12-11T21:09:24+01:00 | 4b919ab | |
0330a57 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 37 | 2019-11-30T09:40:12+01:00 | ||
b3a84f2 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 37 | 2019-11-30T23:18:05+01:00 | ||
9a74315 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 119 | 2019-12-11T20:54:23+01:00 | 7c528dd | |
6f029fe | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 40 | 2019-12-11T21:57:33+01:00 | b3a84f2 | |
98a6f35 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 118 | 2019-12-11T20:23:57+01:00 | 6ceca70 | |
56b2deb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 118 | 2019-12-11T20:14:02+01:00 | 151ae7c | |
2ca65d3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 118 | 2019-12-11T20:07:26+01:00 | 90948c0 | |
5c445d0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 118 | 2019-12-11T20:02:36+01:00 | 7d15790 | |
e7a3c99 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 118 | 2019-12-07T23:44:35+01:00 | 1ab5f7d | |
f75ccf5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 118 | 2019-12-07T19:47:02+01:00 | bf316d2 | |
0a22917 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 118 | 2019-12-06T02:11:32+01:00 | fd1cd02 | |
1cb3f2c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 118 | 2019-11-30T17:13:50+01:00 | 6b19b13 | |
6b19b13 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 118 | 2019-11-29T19:35:29+01:00 | ||
90948c0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 118 | 2019-11-30T23:30:55+01:00 |
Found 26 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i, 59c01c002953c422d4be2154bb5e09b5ab70235e1921dc0ea47ecb7a85dad5de
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/59c01c002953c422d4be2154bb5e09b5ab70235e1921dc0ea47ecb7a85dad5de.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
dd65931 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T07:26 CET (sv-comp) | ||
3be44a0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 37 | 2018-12-08T23:44:34+01:00 | dd65931 | |
4844d09 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 41 | 2018-12-05T17:00:01+01:00 | ||
d1179c9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 119 | 2018-12-08T05:01:50+01:00 | aae8205 | |
f43dafe | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 119 | 2018-12-06T09:14:19+01:00 | 12f9a4f | |
4fbfcde | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 41 | 2018-12-06T23:30:58+01:00 | ||
4fea1b8 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 38 | 2018-12-08T09:00:45+01:00 | 4fbfcde | |
4ae54cf | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 119 | 2018-12-07T09:23:44+01:00 | e16fa54 | |
50b55a1 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 37 | 2018-12-07T01:23:48+01:00 | 464068f | |
f442007 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 38 | 2018-12-06T09:48:08+01:00 | 4844d09 | |
d5d9e07 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 119 | 2018-12-06T10:19:20+01:00 | 0b335ff | |
750408a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T05:33 CET (sv-comp) | ||
73bbc0b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T07:05:41 | ||
a6b083e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 118 | 2018-12-07T04:21:40+01:00 | ||
2e917ea | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-10T19:38:29+01:00 | de1e3b1 | |
1568a81 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-09T20:15:18+01:00 | 8196ea3 | |
25beb35 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-09T19:55:39+01:00 | c98db4d | |
c461662 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-09T17:13:10+01:00 | 29c9f12 | |
21c4a70 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-08T22:49:19+01:00 | 750408a | |
a815458 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-08T21:38:50+01:00 | 73bbc0b | |
44a7d23 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-08T05:13:55+01:00 | a6b083e | |
fe0b385 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-08T04:17:39+01:00 | 067ae2e | |
c722466 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-07T17:43:37+01:00 | c36441f | |
a6f1c83 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-06T09:28:50+01:00 | 352ba30 | |
fe061cd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-06T08:45:31+01:00 | bbe794c | |
bbe794c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 118 | 2018-12-06T02:44:59+01:00 |
Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i, 59c01c002953c422d4be2154bb5e09b5ab70235e1921dc0ea47ecb7a85dad5de
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/59c01c002953c422d4be2154bb5e09b5ab70235e1921dc0ea47ecb7a85dad5de.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_outl_true-unreach-call_false-valid-memtrack.i, 59c01c002953c422d4be2154bb5e09b5ab70235e1921dc0ea47ecb7a85dad5de
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/59c01c002953c422d4be2154bb5e09b5ab70235e1921dc0ea47ecb7a85dad5de.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |