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/ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c |
programSHA | 0a96af1128247617bc94cc042d9c99bdf576fb890db5347a9a1e35be1aa2cb6d |
witnessName | results-verified/cbmc.2017-12-01_1300.logfiles/sv-comp18.kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c.files/witness.graphml |
witnessSHA | 22fc0b0274e82326416941378e882afe894cf7d06db7784f9c429e611b7bb070 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-01T16:33 CET (sv-comp) |
producer | CBMC |
program-sha256 | 0a96af1128247617bc94cc042d9c99bdf576fb890db5347a9a1e35be1aa2cb6d |
programfile | ../../sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c |
programhash | e107441daffe219fcef86523aff14082b11c5fb6 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(F end) ) |
witness-file | witnessFileByHash/22fc0b0274e82326416941378e882afe894cf7d06db7784f9c429e611b7bb070.graphml |
witness-sha256 | 22fc0b0274e82326416941378e882afe894cf7d06db7784f9c429e611b7bb070 |
witness-size | 151970 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 0a96af1128247617bc94cc042d9c99bdf576fb890db5347a9a1e35be1aa2cb6d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/0a96af1128247617bc94cc042d9c99bdf576fb890db5347a9a1e35be1aa2cb6d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 0a96af1128247617bc94cc042d9c99bdf576fb890db5347a9a1e35be1aa2cb6d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/0a96af1128247617bc94cc042d9c99bdf576fb890db5347a9a1e35be1aa2cb6d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 0a96af1128247617bc94cc042d9c99bdf576fb890db5347a9a1e35be1aa2cb6d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/0a96af1128247617bc94cc042d9c99bdf576fb890db5347a9a1e35be1aa2cb6d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 0a96af1128247617bc94cc042d9c99bdf576fb890db5347a9a1e35be1aa2cb6d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/0a96af1128247617bc94cc042d9c99bdf576fb890db5347a9a1e35be1aa2cb6d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 0a96af1128247617bc94cc042d9c99bdf576fb890db5347a9a1e35be1aa2cb6d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/0a96af1128247617bc94cc042d9c99bdf576fb890db5347a9a1e35be1aa2cb6d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 26 witnesses for program sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 0a96af1128247617bc94cc042d9c99bdf576fb890db5347a9a1e35be1aa2cb6d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/0a96af1128247617bc94cc042d9c99bdf576fb890db5347a9a1e35be1aa2cb6d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4279cd9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T20:27 CET (sv-comp) | ||
fa23e9d | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 75 | 2018-12-06T22:29:10+01:00 | ||
3bdae12 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 75 | 2018-12-06T02:41:15+01:00 | ||
6b6861d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 4 | 2018-12-08T04:25 CET (sv-comp) | ||
b063709 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 20 | 2018-12-08T16:27:19 | ||
47cddb2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 43 | 2018-12-07T01:14 CET (sv-comp) | ||
2b6791e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 42 | 2018-12-10T17:44:29+01:00 | ||
9ae356e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 40 | 2018-12-07T23:01:32+01:00 | ||
7766f1d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 45 | 2018-12-10T20:35:56+01:00 | 2b6791e | |
49bf3d2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 45 | 2018-12-09T20:53:19+01:00 | 36119e9 | |
c20d76b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 45 | 2018-12-09T20:37:31+01:00 | cda9645 | |
057d690 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 45 | 2018-12-09T18:21:09+01:00 | 1c004c1 | |
23318ef | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 45 | 2018-12-08T23:43:41+01:00 | 6b6861d | |
72f62f4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 46 | 2018-12-08T22:11:01+01:00 | b063709 | |
0fb54ab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 45 | 2018-12-08T09:01:08+01:00 | 9ae356e | |
8f51fa9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 45 | 2018-12-08T05:02:35+01:00 | 08f67f2 | |
6175864 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 46 | 2018-12-07T17:44:30+01:00 | 47cddb2 | |
2a80237 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 45 | 2018-12-06T10:17:15+01:00 | 36eed08 | |
aa522ff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 45 | 2018-12-06T09:48:05+01:00 | ff4252d | |
03c4d98 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 46 | 2018-12-06T09:18:42+01:00 | fb7c1af | |
ff4252d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 40 | 2018-12-05T14:07:37+01:00 | ||
63b51f1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 75 | 2018-12-09T20:20:50+01:00 | 3362063 | |
9bf854d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 75 | 2018-12-06T09:40:42+01:00 | 6f6c67f | |
aafd62e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 75 | 2018-12-06T09:16:50+01:00 | 256c958 | |
9ba2ba2 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T13:45 CET (sv-comp) | ||
da1aea0 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T08:59 CET (sv-comp) |
Found 28 witnesses for program sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 0a96af1128247617bc94cc042d9c99bdf576fb890db5347a9a1e35be1aa2cb6d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/0a96af1128247617bc94cc042d9c99bdf576fb890db5347a9a1e35be1aa2cb6d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
fcdc4ce | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-03T00:11 CET (sv-comp) | ||
6e02003 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.6.1-svn | 65 | 2017-12-01T09:23:17+01:00 | ||
5abfc91 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 75 | 2017-12-01T08:23:39+01:00 | ||
d8349c8 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T11:25:27.409711 | ||
9bcd735 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T23:04:15.005432 | ||
fa9fa56 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Taipan | 157 | 2017-12-03T06:54Z | ||
97c6c67 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Kojak | 264 | 2017-12-03T04:23Z | ||
55f836e | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CBMC | 152 | 2017-12-01T08:30 CET (sv-comp) | ||
3aa1b4d | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Automizer | 157 | 2017-12-03T04:12Z | ||
540b0e1 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | 2LS | 502 | 2017-12-01T08:19 CET (sv-comp) | ||
6c80acf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 69 | 2017-12-03T00:38Z | ||
5785cec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 3 | 2017-12-01T22:46 CET (sv-comp) | ||
2ed5f84 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 70 | 2017-12-02T13:27Z | ||
d6867e8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 5 | 2017-12-01T21:08:12.855928 | ||
d128b07 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 5 | 2017-12-01T18:39:48.420671 | ||
dd0eba6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 25 | 2017-12-01T17:04 CET (sv-comp) | ||
9748ef1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 25 | 2017-12-01T00:40 CET (sv-comp) | ||
eb08ea0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn | 42 | 2017-12-03T03:25:21+01:00 | ||
c08ef06 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 37 | 2017-11-30T21:16:35+01:00 | ||
580ca4d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 63 | 2017-11-30T20:49:44+01:00 | ||
e1f1ffd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 20 | 2017-12-02T07:02:21+01:00 | ||
721766a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 43 | 2017-11-30T22:55 CET (sv-comp) | ||
f5ca8bf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 69 | 2017-12-02T18:02Z | ||
31aaeb9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 43 | 2017-11-30T22:40 CET (sv-comp) | ||
a5ddd0e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T23:58:14.320289 | ||
070ad15 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T13:22:26.752506 | ||
22fc0b0 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 152 | 2017-12-01T16:33 CET (sv-comp) | ||
35b73e3 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 490 | 2017-12-01T13:30 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 0a96af1128247617bc94cc042d9c99bdf576fb890db5347a9a1e35be1aa2cb6d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/0a96af1128247617bc94cc042d9c99bdf576fb890db5347a9a1e35be1aa2cb6d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |