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_true-unreach-call_true-valid-memsafety_true-termination.cil.c |
programSHA | d823d75b4fb61b836b1ea4370b827655ac54b948b1436d752532e88a55430eb1 |
witnessName | results-verified/veriabs.2018-12-10_1650.logfiles/sv-comp19_prop-reachsafety.kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c.files/witness.graphml |
witnessSHA | 4908c733fac4afb51d9f018c814b5b2f6f8ceddee6ef85def18997fe44de7fa5 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-10T17:28Z |
producer | Automizer |
programfile | /home/benchexec/ar_abs_temp/kbfiltr_simpl2_true_unreach_call_true_valid_memsafety_true_termination_cil_c.c |
programhash | 411af8a324a718637cdc1e76e82ebb1de5e49e9c |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/4908c733fac4afb51d9f018c814b5b2f6f8ceddee6ef85def18997fe44de7fa5.graphml |
witness-sha256 | 4908c733fac4afb51d9f018c814b5b2f6f8ceddee6ef85def18997fe44de7fa5 |
witness-size | 156244 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c, d823d75b4fb61b836b1ea4370b827655ac54b948b1436d752532e88a55430eb1
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/d823d75b4fb61b836b1ea4370b827655ac54b948b1436d752532e88a55430eb1.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_true-unreach-call_true-valid-memsafety_true-termination.cil.c, d823d75b4fb61b836b1ea4370b827655ac54b948b1436d752532e88a55430eb1
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/d823d75b4fb61b836b1ea4370b827655ac54b948b1436d752532e88a55430eb1.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_true-unreach-call_true-valid-memsafety_true-termination.cil.c, d823d75b4fb61b836b1ea4370b827655ac54b948b1436d752532e88a55430eb1
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/d823d75b4fb61b836b1ea4370b827655ac54b948b1436d752532e88a55430eb1.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_true-unreach-call_true-valid-memsafety_true-termination.cil.c, d823d75b4fb61b836b1ea4370b827655ac54b948b1436d752532e88a55430eb1
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/d823d75b4fb61b836b1ea4370b827655ac54b948b1436d752532e88a55430eb1.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_true-unreach-call_true-valid-memsafety_true-termination.cil.c, d823d75b4fb61b836b1ea4370b827655ac54b948b1436d752532e88a55430eb1
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/d823d75b4fb61b836b1ea4370b827655ac54b948b1436d752532e88a55430eb1.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 23 witnesses for program sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c, d823d75b4fb61b836b1ea4370b827655ac54b948b1436d752532e88a55430eb1
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/d823d75b4fb61b836b1ea4370b827655ac54b948b1436d752532e88a55430eb1.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
5cbd7f0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T05:38 CET (sv-comp) | ||
f69138d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 74 | 2018-12-06T22:14:46+01:00 | ||
744b7f4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-05T20:07:35+01:00 | ||
50a06ad | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T20:26 CET (sv-comp) | ||
e5ba1b3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T04:53:00 | ||
5b68995 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T03:31 CET (sv-comp) | ||
be4bf16 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 74 | 2018-12-06T13:23:08+01:00 | ||
3850825 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-10T19:35:23+01:00 | 4908c73 | |
ba4c9c5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-09T20:30:34+01:00 | 82244ac | |
7117e79 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-09T20:04:25+01:00 | 6a78ca7 | |
9bf83e1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-09T19:59:41+01:00 | 9288bbd | |
fa0d7c7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-08T23:08:22+01:00 | 50a06ad | |
7fa02b6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-08T21:42:36+01:00 | e5ba1b3 | |
c16071b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-08T06:47:21+01:00 | be4bf16 | |
6d29d7b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-08T04:12:56+01:00 | 1204829 | |
56076ac | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-07T16:39:18+01:00 | 5b68995 | |
629e4c4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-06T09:28:21+01:00 | ee03931 | |
99205b6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-06T08:45:25+01:00 | bf70ace | |
1c1c152 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-06T08:23:58+01:00 | 2b86d80 | |
bf70ace | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-06T07:17:16+01:00 | ||
b758442 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 74 | 2018-12-06T07:16:32+01:00 | b744867 | |
a220b6e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T15:55 CET (sv-comp) | ||
75993eb | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T15:08 CET (sv-comp) |
Found 43 witnesses for program sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c, d823d75b4fb61b836b1ea4370b827655ac54b948b1436d752532e88a55430eb1
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/d823d75b4fb61b836b1ea4370b827655ac54b948b1436d752532e88a55430eb1.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d5bb617 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-03T00:27 CET (sv-comp) | ||
a203496 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.6.1-svn | 63 | 2017-12-01T09:39:33+01:00 | ||
4122495 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 74 | 2017-12-01T08:24:26+01:00 | ||
92a1feb | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T10:53:04.781098 | ||
2afd0e7 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T23:32:48.306258 | ||
09eb196 | 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 | 156 | 2017-12-03T06:53Z | ||
3e740ab | 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 | 263 | 2017-12-03T03:58Z | ||
1166fa2 | 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:19 CET (sv-comp) | ||
89053cb | 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 | 156 | 2017-12-03T04:14Z | ||
f3b250a | 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 | 499 | 2017-12-01T08:21 CET (sv-comp) | ||
532c392 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 156 | 2017-12-02T20:56Z | ||
d2bafb6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T07:14 CET (sv-comp) | ||
b32e2fc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 166 | 2017-12-02T17:53Z | ||
f0a4482 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T23:50:35.400185 | ||
459cee5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T08:02:20.689719 | ||
f1a73a9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T18:47:24.473548 | ||
fc62ae8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T09:04:10.276349 | ||
ff76c65 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 185 | 2017-12-01T19:53 CET (sv-comp) | ||
f1d2a13 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 74 | 2017-12-02T22:23:03+01:00 | ||
a995231 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-11-30T18:25:43+01:00 | ||
b2b8b0e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 74 | 2017-12-03T06:51:18+01:00 | 734250b | |
fbac4bb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 74 | 2017-12-03T04:21:00+01:00 | 11224e4 | |
2f97096 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 74 | 2017-12-03T02:55:00+01:00 | 4201ea2 | |
2e647c9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 74 | 2017-12-03T02:29:51+01:00 | ccad76e | |
213d63a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 74 | 2017-12-02T20:17:41+01:00 | b71a062 | |
47d86ee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 74 | 2017-12-02T15:02:13+01:00 | 96c2958 | |
898cd37 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 74 | 2017-12-02T08:46:57+01:00 | 53e8875 | |
5ec704c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 74 | 2017-12-01T22:32:59+01:00 | b192d02 | |
e9c40f3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 74 | 2017-12-01T08:13:32+01:00 | 992cce7 | |
db34824 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 74 | 2017-12-01T07:12:48+01:00 | d305485 | |
0541d50 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 74 | 2017-12-01T06:50:50+01:00 | 529cd3e | |
6a93cef | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 74 | 2017-12-01T06:41:35+01:00 | aed2d2d | |
872402d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 74 | 2017-12-01T05:24:30+01:00 | fc28680 | |
0e3fef9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 74 | 2017-12-01T05:15:05+01:00 | 93c269d | |
a266c09 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 74 | 2017-11-30T15:54:15+01:00 | ||
e0a3f50 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 143 | 2017-12-01T03:09:53+01:00 | ||
7924700 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 74 | 2017-11-30T15:06:32+01:00 | ||
4f9cc88 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 46 | 2017-12-01T22:05:23+01:00 | ||
6e3216a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 152 | 2017-11-30T16:30 CET (sv-comp) | ||
ab59895 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 156 | 2017-12-02T00:27Z | ||
367fc62 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 487 | 2017-11-30T18:06 CET (sv-comp) | ||
351af15 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 152 | 2017-12-01T13:32 CET (sv-comp) | ||
12292fa | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 487 | 2017-12-01T15:21 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c, d823d75b4fb61b836b1ea4370b827655ac54b948b1436d752532e88a55430eb1
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/d823d75b4fb61b836b1ea4370b827655ac54b948b1436d752532e88a55430eb1.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |