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/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c |
programSHA | 41f3ae880f1c5fccef1a5a43afa9a07d5a1500604f4f27daf5f9a587bf3226b6 |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-utaipan.2018-12-09_2052.logfiles/sv-comp19_prop-reachsafety.floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c.files/witness.graphml |
witnessSHA | 2b95914c642fce94c384b172b316dcf918c5728c7c7d6ccfcd8596eaf41a31e1 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-09T20:53:12+01:00 |
inputwitnesshash | 61bb1da47401c13f9f98a103c012e1d340aae7016e7d317a69f4f04d984f3675 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 41f3ae880f1c5fccef1a5a43afa9a07d5a1500604f4f27daf5f9a587bf3226b6 |
programfile | ../../sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c |
programhash | 41f3ae880f1c5fccef1a5a43afa9a07d5a1500604f4f27daf5f9a587bf3226b6 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/2b95914c642fce94c384b172b316dcf918c5728c7c7d6ccfcd8596eaf41a31e1.graphml |
witness-sha256 | 2b95914c642fce94c384b172b316dcf918c5728c7c7d6ccfcd8596eaf41a31e1 |
witness-size | 116088 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, 41f3ae880f1c5fccef1a5a43afa9a07d5a1500604f4f27daf5f9a587bf3226b6).
Found 0 witnesses for program sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 41f3ae880f1c5fccef1a5a43afa9a07d5a1500604f4f27daf5f9a587bf3226b6
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/41f3ae880f1c5fccef1a5a43afa9a07d5a1500604f4f27daf5f9a587bf3226b6.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/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 41f3ae880f1c5fccef1a5a43afa9a07d5a1500604f4f27daf5f9a587bf3226b6
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/41f3ae880f1c5fccef1a5a43afa9a07d5a1500604f4f27daf5f9a587bf3226b6.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/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 41f3ae880f1c5fccef1a5a43afa9a07d5a1500604f4f27daf5f9a587bf3226b6
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/41f3ae880f1c5fccef1a5a43afa9a07d5a1500604f4f27daf5f9a587bf3226b6.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/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 41f3ae880f1c5fccef1a5a43afa9a07d5a1500604f4f27daf5f9a587bf3226b6
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/41f3ae880f1c5fccef1a5a43afa9a07d5a1500604f4f27daf5f9a587bf3226b6.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/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 41f3ae880f1c5fccef1a5a43afa9a07d5a1500604f4f27daf5f9a587bf3226b6
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/41f3ae880f1c5fccef1a5a43afa9a07d5a1500604f4f27daf5f9a587bf3226b6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 25 witnesses for program sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 41f3ae880f1c5fccef1a5a43afa9a07d5a1500604f4f27daf5f9a587bf3226b6
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/41f3ae880f1c5fccef1a5a43afa9a07d5a1500604f4f27daf5f9a587bf3226b6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e3c7797 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T02:48 CET (sv-comp) | ||
dd422b3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 116 | 2018-12-07T10:25:12+01:00 | ||
136a599 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 116 | 2018-12-05T11:46:33+01:00 | ||
9a60147 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 4 | 2018-12-08T12:46 CET (sv-comp) | ||
1c924b7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 26 | 2018-12-08T16:53:51 | ||
eac0bea | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 64 | 2018-12-07T09:10 CET (sv-comp) | ||
3a8d7c5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 59 | 2018-12-10T17:21:46+01:00 | ||
f1a3d7a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 53 | 2018-12-07T14:30:25+01:00 | ||
731a310 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 64 | 2018-12-10T20:34:53+01:00 | 3a8d7c5 | |
ad45448 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 63 | 2018-12-09T18:21:34+01:00 | 70b8417 | |
9e16b1d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 64 | 2018-12-08T23:43:30+01:00 | 9a60147 | |
f978e67 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 65 | 2018-12-08T22:07:27+01:00 | 1c924b7 | |
cde215c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 63 | 2018-12-08T08:37:29+01:00 | f1a3d7a | |
3c21149 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 63 | 2018-12-08T04:59:52+01:00 | fc11d00 | |
81cc191 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 72 | 2018-12-07T17:43:53+01:00 | eac0bea | |
55e6b62 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 63 | 2018-12-06T10:19:59+01:00 | f89b905 | |
d432be4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 63 | 2018-12-06T09:48:37+01:00 | 5735def | |
46e8b22 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 64 | 2018-12-06T09:11:47+01:00 | 2903060 | |
5735def | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 53 | 2018-12-06T04:47:21+01:00 | ||
2b95914 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 116 | 2018-12-09T20:53:12+01:00 | 61bb1da | |
da255e1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 116 | 2018-12-09T20:36:24+01:00 | db3af8e | |
0859756 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 116 | 2018-12-06T09:41:46+01:00 | e10878b | |
3e34a38 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 116 | 2018-12-06T09:18:06+01:00 | be440a9 | |
0127c23 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T00:47 CET (sv-comp) | ||
5b04605 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T13:11 CET (sv-comp) |
Found 28 witnesses for program sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 41f3ae880f1c5fccef1a5a43afa9a07d5a1500604f4f27daf5f9a587bf3226b6
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/41f3ae880f1c5fccef1a5a43afa9a07d5a1500604f4f27daf5f9a587bf3226b6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3cd4532 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T23:42 CET (sv-comp) | ||
ae8edb1 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T11:50:46.045484 | ||
8e6a1f6 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T23:17:24.293371 | ||
df70b3b | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.6.1-svn | 105 | 2017-12-01T09:33:48+01:00 | ||
0b7b87b | 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 | 280 | 2017-12-03T06:53Z | ||
4ae6fda | 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 | 459 | 2017-12-03T03:59Z | ||
811eb16 | 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 | 285 | 2017-12-01T08:30 CET (sv-comp) | ||
791ccba | 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 | 280 | 2017-12-03T04:28Z | ||
b6758bc | 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 | 1013 | 2017-12-01T08:19 CET (sv-comp) | ||
6b2c1b8 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 116 | 2017-12-01T08:28:00+01:00 | ||
41d30a9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 95 | 2017-12-03T02:44Z | ||
142a7e4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 4 | 2017-12-02T09:29 CET (sv-comp) | ||
118c7c9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 96 | 2017-12-02T11:41Z | ||
919fc91 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 7 | 2017-12-02T00:18:48.870020 | ||
fe277c4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 7 | 2017-12-01T14:55:00.316955 | ||
fb54482 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 39 | 2017-12-01T15:42 CET (sv-comp) | ||
b5ee215 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 39 | 2017-12-01T04:39 CET (sv-comp) | ||
4652b97 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn | 59 | 2017-12-02T21:53:24+01:00 | ||
27d5cb8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 49 | 2017-11-30T19:29:33+01:00 | ||
d09b6a5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 92 | 2017-11-30T21:43:18+01:00 | ||
3b26a5e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 23 | 2017-12-01T20:28:51+01:00 | ||
524dc8b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 66 | 2017-12-01T03:03 CET (sv-comp) | ||
de9a441 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 95 | 2017-12-02T16:06Z | ||
f535db2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 59 | 2017-11-30T13:54 CET (sv-comp) | ||
76186e5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T00:17:54.685041 | ||
4fc5223 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T13:32:21.542841 | ||
f7b0014 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 285 | 2017-12-01T17:56 CET (sv-comp) | ||
d94d5bd | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 995 | 2017-12-01T15:57 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 41f3ae880f1c5fccef1a5a43afa9a07d5a1500604f4f27daf5f9a587bf3226b6
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/41f3ae880f1c5fccef1a5a43afa9a07d5a1500604f4f27daf5f9a587bf3226b6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |