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_true-unreach-call_true-valid-memsafety_true-termination.cil.c |
programSHA | ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e |
witnessName | results-verified/symbiotic.2018-12-07_2142.logfiles/sv-comp19_prop-reachsafety.floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c.files/witness.graphml |
witnessSHA | 84f4abf14e426d203530936095e68440315a1c5cdd6d1ecf440c4a5c1e298b7d |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T09:17 CET (sv-comp) |
producer | Symbiotic |
program-sha256 | ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_f68d9cd5-5b6c-4997-b810-58d526619826/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c |
programhash | ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/84f4abf14e426d203530936095e68440315a1c5cdd6d1ecf440c4a5c1e298b7d.graphml |
witness-sha256 | 84f4abf14e426d203530936095e68440315a1c5cdd6d1ecf440c4a5c1e298b7d |
witness-size | 820 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e).
Found 0 witnesses for program sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c, ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e.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_true-unreach-call_true-valid-memsafety_true-termination.cil.c, ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e.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_true-unreach-call_true-valid-memsafety_true-termination.cil.c, ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e.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_true-unreach-call_true-valid-memsafety_true-termination.cil.c, ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e.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_true-unreach-call_true-valid-memsafety_true-termination.cil.c, ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e.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/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c, ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
bc2a503 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T04:21 CET (sv-comp) | ||
289502a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 116 | 2018-12-05T10:49:33+01:00 | ||
1eb400f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 116 | 2018-12-07T09:40:35+01:00 | ||
84f4abf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T09:17 CET (sv-comp) | ||
30b1565 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T04:42:23 | ||
b97a92b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T00:01 CET (sv-comp) | ||
26bb2aa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7 | 119 | 2018-12-10T18:19:30+01:00 | ||
8bf7654 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 116 | 2018-12-06T21:16:43+01:00 | ||
bd568ff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 116 | 2018-12-10T19:56:23+01:00 | 26bb2aa | |
6187c34 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 116 | 2018-12-09T20:20:35+01:00 | a64b811 | |
d19fc01 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 116 | 2018-12-09T17:13:05+01:00 | 21684df | |
236e244 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 116 | 2018-12-08T23:14:55+01:00 | 84f4abf | |
701daf4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 116 | 2018-12-08T21:22:07+01:00 | 30b1565 | |
7081cec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 116 | 2018-12-08T05:52:57+01:00 | 8bf7654 | |
282ec01 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 116 | 2018-12-08T02:34:20+01:00 | f5345e5 | |
17d139d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 116 | 2018-12-07T16:37:54+01:00 | b97a92b | |
70d4aa6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 116 | 2018-12-06T09:29:05+01:00 | 73f22e4 | |
100c9c7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 116 | 2018-12-06T09:04:22+01:00 | 57e5deb | |
6a93daf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 116 | 2018-12-06T08:29:04+01:00 | 8c00647 | |
16abcf8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 116 | 2018-12-06T07:34:20+01:00 | fe1d977 | |
57e5deb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 116 | 2018-12-05T14:03:06+01:00 | ||
0ee47aa | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T07:05 CET (sv-comp) | ||
0205bac | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T10:05 CET (sv-comp) |
Found 35 witnesses for program sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c, ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ac8cdc0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2017-12-03T00:24 CET (sv-comp) | ||
db04fc5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.6.1-svn | 101 | 2017-12-01T09:12:51+01:00 | ||
3c0773d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 116 | 2017-12-01T08:25:48+01:00 | ||
fb35908 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T11:14:24.411523 | ||
e607a41 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T23:22:08.685403 | ||
d93dc02 | 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:54Z | ||
398e31b | 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 | 458 | 2017-12-03T03:43Z | ||
1b485f7 | 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 | 284 | 2017-12-01T08:21 CET (sv-comp) | ||
dd4e42a | 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:14Z | ||
8f81d58 | 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 | 1009 | 2017-12-01T08:23 CET (sv-comp) | ||
1b3acd1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T00:48 CET (sv-comp) | ||
8d4d790 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T01:03:12.072466 | ||
3957e23 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T15:07:33.140160 | ||
e7006da | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T02:58:22.869421 | ||
944d165 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T18:12:12.869330 | ||
6ef3710 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 342 | 2017-12-01T20:42 CET (sv-comp) | ||
4475583 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 119 | 2017-12-02T22:49:58+01:00 | ||
56f2d87 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-11-30T18:36:36+01:00 | ||
ecebf16 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 116 | 2017-12-03T04:03:12+01:00 | eea62d0 | |
a4b98f2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 116 | 2017-12-03T00:07:03+01:00 | 89afe4e | |
76875aa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 116 | 2017-12-02T20:13:43+01:00 | a18bfc0 | |
edf4997 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 116 | 2017-12-02T14:56:32+01:00 | efd70a7 | |
b6817fc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 116 | 2017-12-02T08:46:46+01:00 | d38b0d9 | |
53375a3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 116 | 2017-12-01T22:37:45+01:00 | 850c7df | |
a65f020 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 116 | 2017-12-01T08:14:03+01:00 | 2f7d200 | |
5bd5202 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 116 | 2017-12-01T06:35:44+01:00 | dce0778 | |
0a4776e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 116 | 2017-12-01T06:01:43+01:00 | fb2bc4d | |
2400231 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 116 | 2017-12-01T05:42:51+01:00 | d59cb71 | |
6ca2810 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 116 | 2017-11-30T13:24:24+01:00 | ||
b198d30 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 98 | 2017-12-01T23:51:16+01:00 | ||
116ef46 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 287 | 2017-12-01T03:36 CET (sv-comp) | ||
2e4cb38 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 280 | 2017-12-02T10:43Z | ||
e547c05 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 991 | 2017-12-01T01:18 CET (sv-comp) | ||
25bd176 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 284 | 2017-12-01T18:54 CET (sv-comp) | ||
a420c87 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 991 | 2017-12-01T14:21 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c, ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |