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/list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i
programSHA da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e
witnessName results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-memsafety.dll_nullified_true-unreach-call_true-valid-memsafety.i.files/witness.graphml
witnessSHA bdd530c59f561a999cb25cf5488dbde9f08d02a6aa67fa17d2769ab083390598

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/bdd530c59f561a999cb25cf5488dbde9f08d02a6aa67fa17d2769ab083390598.json

Key Value
architecture 32bit
creationtime 2018-12-06T06:23:43.651819
producer DepthK v3.0
programfile /tmp/vcloud-vcloud-master/worker/working_dir_8ba97d39-5111-4cfb-99ba-7a719b49a415/sv-benchmarks/c/list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i
programhash 8a7557f09f8e1fbed7221a578047e51fd09f2dbf
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) )
witness-file witnessFileByHash/bdd530c59f561a999cb25cf5488dbde9f08d02a6aa67fa17d2769ab083390598.graphml
witness-sha256 bdd530c59f561a999cb25cf5488dbde9f08d02a6aa67fa17d2769ab083390598
witness-size 3511
witness-type correctness_witness

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

Trying to find witnesses for program (da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e, sv-benchmarks/c/list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i, da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e.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 (da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e, sv-benchmarks/c/list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i, da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e.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 (da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e, sv-benchmarks/c/list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i, da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e.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 (da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e, sv-benchmarks/c/list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i, da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e.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 (da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e, sv-benchmarks/c/list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i).

Found 16 witnesses for program sv-benchmarks/c/list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i, da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 105f31a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 10 2019-12-01T02:06:07+01:00
Download c2aca38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.9 10 2019-11-30T05:27:17+01:00
Download 1c670a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T01:09 CET (comp)
Download 2332bac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 10 2019-12-11T20:15:24+01:00 Download 48bc374
Download 6c10fc6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 10 2019-12-11T20:08:05+01:00 Download 5b14996
Download de60d6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 10 2019-12-11T20:02:27+01:00 Download 7577f72
Download cb4e92a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 10 2019-12-08T00:54:27+01:00 Download ed642fa
Download 27e9e99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 10 2019-12-07T23:46:03+01:00 Download b82923d
Download 49940ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 10 2019-12-06T02:06:55+01:00 Download 380562b
Download f7ec1aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 10 2019-12-05T19:13:30+01:00 Download 1eaf1b5
Download f83ffc2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 10 2019-12-04T02:07:33+01:00 Download 1c670a6
Download 4ede1f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 10 2019-11-30T19:29:29+01:00 Download b3dac51
Download 3f66adf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 10 2019-11-30T16:12:27+01:00 Download 28dcbb9
Download 28dcbb9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 12 2019-11-29T19:44:51+01:00
Download ed642fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 11 2019-12-07T20:24:32+01:00
Download 5b14996 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 10 2019-12-01T02:19:43+01:00

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

Trying to find witnesses for program (da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e, sv-benchmarks/c/list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i).

Found 21 witnesses for program sv-benchmarks/c/list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i, da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b2789b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2018-12-08T13:36 CET (sv-comp)
Download 2a94dea Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 10 2018-12-07T15:31:32+01:00
Download fbbcf3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-06T07:13:46+01:00
Download ec0f0d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T11:37 CET (sv-comp)
Download 7c33850 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T03:36:19
Download 46a8985 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T09:54 CET (sv-comp)
Download e10e9a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 11 2018-12-10T18:01:56+01:00
Download 9d11c97 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 13 2018-12-07T07:14:43+01:00
Download 6b95061 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-10T20:14:08+01:00 Download e10e9a3
Download 15cb604 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-10T10:32:02+01:00 Download 1cdb2d2
Download 3e773e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-08T23:14:45+01:00 Download ec0f0d0
Download 63956db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-08T21:29:40+01:00 Download 7c33850
Download 607dece Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-08T06:40:26+01:00 Download 9d11c97
Download 36783fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-08T03:02:06+01:00 Download 78b89b3
Download d223291 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-08T01:59:56+01:00 Download 1cdb2d2
Download d87fe12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-07T16:38:34+01:00 Download 46a8985
Download 648bb22 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-07T08:52:58+01:00 Download f246324
Download 904c99d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-06T09:29:12+01:00 Download b273554
Download 48ac722 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-06T09:01:14+01:00 Download a4d9c08
Download 8c6c28c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-06T08:29:54+01:00 Download 9502deb
Download a4d9c08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-05T15:52:58+01:00

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

Trying to find witnesses for program (da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e, sv-benchmarks/c/list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i, da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e.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 '17

Trying to find witnesses for program (da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e, sv-benchmarks/c/list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i, da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/da0d5aa2a3a3b4f12b459e7a1c99ef7428963e5c64a2865d7bd55c2cf855e49e.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness