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/ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 0705dc4f87828fe23477849ee500ca109b92481aa33e7c5eb2e2979158175ad0
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/0705dc4f87828fe23477849ee500ca109b92481aa33e7c5eb2e2979158175ad0.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_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 0705dc4f87828fe23477849ee500ca109b92481aa33e7c5eb2e2979158175ad0
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/0705dc4f87828fe23477849ee500ca109b92481aa33e7c5eb2e2979158175ad0.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_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 0705dc4f87828fe23477849ee500ca109b92481aa33e7c5eb2e2979158175ad0
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/0705dc4f87828fe23477849ee500ca109b92481aa33e7c5eb2e2979158175ad0.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_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 0705dc4f87828fe23477849ee500ca109b92481aa33e7c5eb2e2979158175ad0
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/0705dc4f87828fe23477849ee500ca109b92481aa33e7c5eb2e2979158175ad0.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_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 0705dc4f87828fe23477849ee500ca109b92481aa33e7c5eb2e2979158175ad0
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/0705dc4f87828fe23477849ee500ca109b92481aa33e7c5eb2e2979158175ad0.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_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 0705dc4f87828fe23477849ee500ca109b92481aa33e7c5eb2e2979158175ad0
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/0705dc4f87828fe23477849ee500ca109b92481aa33e7c5eb2e2979158175ad0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c9aff9a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T05:03 CET (sv-comp) | ||
bea13e0 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 85 | 2018-12-08T02:17:13+01:00 | ||
b17d688 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 85 | 2018-12-06T03:27:50+01:00 | ||
6e20692 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 3 | 2018-12-08T14:48 CET (sv-comp) | ||
6e8842a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 26 | 2018-12-08T11:11:45 | ||
83cca93 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 62 | 2018-12-07T05:17 CET (sv-comp) | ||
a8d0198 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 57 | 2018-12-10T17:22:27+01:00 | ||
c485138 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 51 | 2018-12-07T07:24:17+01:00 | ||
039a7b0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 61 | 2018-12-10T20:34:55+01:00 | a8d0198 | |
3f2a0c7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 60 | 2018-12-09T18:21:36+01:00 | 6038697 | |
3debeac | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 61 | 2018-12-08T23:44:19+01:00 | 6e20692 | |
2e1fe6d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 62 | 2018-12-08T22:11:05+01:00 | 6e8842a | |
9125a28 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 60 | 2018-12-08T08:28:26+01:00 | c485138 | |
a73f4f2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 62 | 2018-12-08T05:00:50+01:00 | 79ca7f1 | |
e4e840a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 70 | 2018-12-07T17:43:17+01:00 | 83cca93 | |
5415d18 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 62 | 2018-12-06T10:19:57+01:00 | b548a12 | |
b1cb9c2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 61 | 2018-12-06T09:48:13+01:00 | 2826809 | |
adc9f33 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 60 | 2018-12-06T09:17:55+01:00 | b6d63b5 | |
2826809 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 51 | 2018-12-05T09:47:04+01:00 | ||
8eab714 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 85 | 2018-12-09T20:53:21+01:00 | 92e7d7a | |
df51f4b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 85 | 2018-12-09T20:39:10+01:00 | cfd775e | |
8c084cf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 85 | 2018-12-06T09:40:39+01:00 | 483204b | |
e9f4cea | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 85 | 2018-12-06T09:11:41+01:00 | 9f73ecd | |
659dd0c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T01:07 CET (sv-comp) | ||
7ad6432 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-06T23:56 CET (sv-comp) |
Found 28 witnesses for program sv-benchmarks/c/ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 0705dc4f87828fe23477849ee500ca109b92481aa33e7c5eb2e2979158175ad0
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/0705dc4f87828fe23477849ee500ca109b92481aa33e7c5eb2e2979158175ad0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9b988be | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T23:25 CET (sv-comp) | ||
612b817 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 85 | 2017-12-01T08:29:18+01:00 | ||
6461145 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T11:35:45.974320 | ||
4c5b2c9 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T23:21:49.390455 | ||
c546141 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.6.1-svn | 74 | 2017-12-01T09:08:50+01:00 | ||
0464586 | 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 | 191 | 2017-12-03T06:53Z | ||
a59d610 | 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 | 315 | 2017-12-03T04:12Z | ||
a695fa1 | 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 | 196 | 2017-12-01T08:20 CET (sv-comp) | ||
ae7f004 | 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 | 191 | 2017-12-03T04:13Z | ||
50e5e92 | 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 | 637 | 2017-12-01T08:19 CET (sv-comp) | ||
378dcd5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 91 | 2017-12-03T02:29Z | ||
06072ce | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 3 | 2017-12-02T11:17 CET (sv-comp) | ||
a237ba1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 7 | 2017-12-02T00:59:42.050630 | ||
e7fb3b0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 7 | 2017-12-01T14:08:19.836048 | ||
f80ad63 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 33 | 2017-12-01T21:33 CET (sv-comp) | ||
e188bb6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 33 | 2017-11-30T21:42 CET (sv-comp) | ||
122449b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn | 57 | 2017-12-02T21:42:15+01:00 | ||
0bd6d7d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 48 | 2017-11-30T11:42:55+01:00 | ||
4d2412b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 88 | 2017-11-30T21:55:36+01:00 | ||
86a3246 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 26 | 2017-12-01T02:56:15+01:00 | ||
d3bf8d3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 21 | 2017-12-02T04:59:05+01:00 | ||
c7831c1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 63 | 2017-11-30T23:42 CET (sv-comp) | ||
bec1d08 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 91 | 2017-12-02T02:15Z | ||
a05bdb5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 57 | 2017-12-01T01:16 CET (sv-comp) | ||
a6f80fa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T23:46:42.951075 | ||
e1d6c8f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T08:09:34.994300 | ||
9b41ef2 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 196 | 2017-12-01T15:57 CET (sv-comp) | ||
8defa5d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 623 | 2017-12-01T15:31 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c, 0705dc4f87828fe23477849ee500ca109b92481aa33e7c5eb2e2979158175ad0
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/0705dc4f87828fe23477849ee500ca109b92481aa33e7c5eb2e2979158175ad0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |