Witness Inspection

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).

View and Validate the Witness

Input Given to this Service about the Witness (URL Query)

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/depthk.2017-11-30_1601.logfiles/sv-comp18.floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c.files/witness.graphml
witnessSHA 56f2d876f3289450c8bc68fc404cc609bc45d9153fd467f711c62e676ae322be

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/56f2d876f3289450c8bc68fc404cc609bc45d9153fd467f711c62e676ae322be.json

Key Value
architecture 32bit
creationtime 2017-11-30T18:36:36+01:00
producer CPAchecker 1.6.1-svn
program-sha256 ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e
programfile /tmp/vcloud-vcloud-master/worker/working_dir_29ee43c9-fd22-486e-86bc-955933825bdd/sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c
programhash 9187bc92090d01e0892e8fd14c7d6a75e3556b66
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/56f2d876f3289450c8bc68fc404cc609bc45d9153fd467f711c62e676ae322be.graphml
witness-sha256 56f2d876f3289450c8bc68fc404cc609bc45d9153fd467f711c62e676ae322be
witness-size 3995
witness-type correctness_witness

Available Results for the Program from Witness Store SV-COMP '24

Trying to find witnesses for program (ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e, sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c).

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

Available Results for the Program from Witness Store SV-COMP '23

Trying to find witnesses for program (ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e, sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c).

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

Available Results for the Program from Witness Store SV-COMP '22

Trying to find witnesses for program (ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e, sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c).

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

Available Results for the Program from Witness Store SV-COMP '21

Trying to find witnesses for program (ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e, sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c).

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

Available Results for the Program from Witness Store SV-COMP '20

Trying to find witnesses for program (ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e, sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c).

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

Available Results for the Program from Witness Store SV-COMP '19

Trying to find witnesses for program (ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e, sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c).

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
Download bc2a503 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2018-12-08T04:21 CET (sv-comp)
Download 289502a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 116 2018-12-05T10:49:33+01:00
Download 1eb400f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 116 2018-12-07T09:40:35+01:00
Download 84f4abf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T09:17 CET (sv-comp)
Download 30b1565 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T04:42:23
Download b97a92b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T00:01 CET (sv-comp)
Download 26bb2aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 119 2018-12-10T18:19:30+01:00
Download 8bf7654 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 116 2018-12-06T21:16:43+01:00
Download bd568ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 116 2018-12-10T19:56:23+01:00 Download 26bb2aa
Download 6187c34 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 116 2018-12-09T20:20:35+01:00 Download a64b811
Download d19fc01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 116 2018-12-09T17:13:05+01:00 Download 21684df
Download 236e244 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 116 2018-12-08T23:14:55+01:00 Download 84f4abf
Download 701daf4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 116 2018-12-08T21:22:07+01:00 Download 30b1565
Download 7081cec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 116 2018-12-08T05:52:57+01:00 Download 8bf7654
Download 282ec01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 116 2018-12-08T02:34:20+01:00 Download f5345e5
Download 17d139d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 116 2018-12-07T16:37:54+01:00 Download b97a92b
Download 70d4aa6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 116 2018-12-06T09:29:05+01:00 Download 73f22e4
Download 100c9c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 116 2018-12-06T09:04:22+01:00 Download 57e5deb
Download 6a93daf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 116 2018-12-06T08:29:04+01:00 Download 8c00647
Download 16abcf8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 116 2018-12-06T07:34:20+01:00 Download fe1d977
Download 57e5deb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 116 2018-12-05T14:03:06+01:00
Download 0ee47aa Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T07:05 CET (sv-comp)
Download 0205bac Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T10:05 CET (sv-comp)

Available Results for the Program from Witness Store SV-COMP '18

Trying to find witnesses for program (ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e, sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c).

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
Download ac8cdc0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2017-12-03T00:24 CET (sv-comp)
Download db04fc5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.6.1-svn 101 2017-12-01T09:12:51+01:00
Download 3c0773d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.6.1-svn 26773 116 2017-12-01T08:25:48+01:00
Download fb35908 Inspect Inspect
Validate
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
Download e607a41 Inspect Inspect
Validate
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
Download d93dc02 Inspect Inspect
Validate
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
Download 398e31b Inspect Inspect
Validate
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
Download 1b485f7 Inspect Inspect
Validate
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)
Download dd4e42a Inspect Inspect
Validate
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
Download 8f81d58 Inspect Inspect
Validate
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)
Download 1b3acd1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T00:48 CET (sv-comp)
Download 8d4d790 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T01:03:12.072466
Download 3957e23 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T15:07:33.140160
Download e7006da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T02:58:22.869421
Download 944d165 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T18:12:12.869330
Download 6ef3710 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 342 2017-12-01T20:42 CET (sv-comp)
Download 4475583 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 119 2017-12-02T22:49:58+01:00
Download 56f2d87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-11-30T18:36:36+01:00
Download ecebf16 Inspect Inspect
Validate
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
Download a4b98f2 Inspect Inspect
Validate
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
Download 76875aa Inspect Inspect
Validate
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
Download edf4997 Inspect Inspect
Validate
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
Download b6817fc Inspect Inspect
Validate
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
Download 53375a3 Inspect Inspect
Validate
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
Download a65f020 Inspect Inspect
Validate
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
Download 5bd5202 Inspect Inspect
Validate
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
Download 0a4776e Inspect Inspect
Validate
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
Download 2400231 Inspect Inspect
Validate
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
Download 6ca2810 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 116 2017-11-30T13:24:24+01:00
Download b198d30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 98 2017-12-01T23:51:16+01:00
Download 116ef46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 287 2017-12-01T03:36 CET (sv-comp)
Download 2e4cb38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 280 2017-12-02T10:43Z
Download e547c05 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 991 2017-12-01T01:18 CET (sv-comp)
Download 25bd176 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 284 2017-12-01T18:54 CET (sv-comp)
Download a420c87 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 991 2017-12-01T14:21 CET (sv-comp)

Available Results for the Program from Witness Store SV-COMP '17

Trying to find witnesses for program (ffd8cf6bad12875b15ba42d835e510e4110e0de61969363a3b97a28034fa604e, sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c).

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