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-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i
programSHA 23106d2be7c2d5ee5e241d7f9aabf0dd10692919878117026edb76306f53c494
witnessName results-verified/map2check.2018-12-06_1220.logfiles/sv-comp19_prop-memsafety.dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i.files/witness.graphml
witnessSHA bc217618477a4b31448a18ec4eac4650b01bdbcc8349614fdf8927b8a7db7e05

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T13:31 CET (sv-comp)
error-specification-length Key 'specification' longer than 100 characters.
producer Map2Check
programfile /tmp/vcloud-vcloud-master/worker/working_dir_c19b84fe-d916-4dcd-873a-d769a1e3176d/bin-2019/map2check/../../sv-benchmarks/c/list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i
programhash b171d8322722cfe50829ea6c9e3bfdd3740068da
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )
witness-file witnessFileByHash/bc217618477a4b31448a18ec4eac4650b01bdbcc8349614fdf8927b8a7db7e05.graphml
witness-sha256 bc217618477a4b31448a18ec4eac4650b01bdbcc8349614fdf8927b8a7db7e05
witness-size 2213
witness-type correctness_witness

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

Trying to find witnesses for program (23106d2be7c2d5ee5e241d7f9aabf0dd10692919878117026edb76306f53c494, sv-benchmarks/c/list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i).

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

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

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

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

Found 17 witnesses for program sv-benchmarks/c/list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i, 23106d2be7c2d5ee5e241d7f9aabf0dd10692919878117026edb76306f53c494
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/23106d2be7c2d5ee5e241d7f9aabf0dd10692919878117026edb76306f53c494.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5fc86f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 13 2019-11-30T03:35:31+01:00
Download 6642e54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 13 2019-12-01T02:21:06+01:00
Download 004c85a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T22:23 CET (comp)
Download b2ee52d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-11T20:42:32+01:00 Download 0430087
Download ed55d72 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-11T20:33:10+01:00 Download e3e760d
Download e194293 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-11T20:17:43+01:00 Download 9281066
Download 9c6f9a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-08T01:27:20+01:00 Download cbe7278
Download 562bd30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-08T00:01:11+01:00 Download 78ad46c
Download 7cb0b05 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-07T19:57:00+01:00 Download d370fe7
Download b71f649 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-06T02:02:02+01:00 Download 329b3d1
Download da0a6a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-05T19:27:29+01:00 Download 5d74883
Download 5f253c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-04T02:22:41+01:00 Download 004c85a
Download 99acd39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-11-30T19:33:57+01:00 Download 2d9f929
Download d8925cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-11-30T17:36:57+01:00 Download 4f62d32
Download 4f62d32 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 16 2019-11-30T03:09:12+01:00
Download cbe7278 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 14 2019-12-07T22:28:34+01:00
Download 0430087 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 13 2019-12-01T05:44:12+01:00

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

Trying to find witnesses for program (23106d2be7c2d5ee5e241d7f9aabf0dd10692919878117026edb76306f53c494, sv-benchmarks/c/list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i).

Found 22 witnesses for program sv-benchmarks/c/list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i, 23106d2be7c2d5ee5e241d7f9aabf0dd10692919878117026edb76306f53c494
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/23106d2be7c2d5ee5e241d7f9aabf0dd10692919878117026edb76306f53c494.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download bfb5b94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2018-12-08T02:17 CET (sv-comp)
Download 035fd65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 13 2018-12-07T08:56:35+01:00
Download b92a87b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-05T19:43:54+01:00
Download ee4d6aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T19:35 CET (sv-comp)
Download 466232d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T12:00:59
Download 910ef60 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T07:47 CET (sv-comp)
Download e482603 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 14 2018-12-10T17:56:18+01:00
Download d408288 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 16 2018-12-07T09:33:13+01:00
Download c01814a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 14 2018-12-10T20:17:26+01:00 Download e482603
Download 97933fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-10T10:31:40+01:00 Download fc321db
Download 46012b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-08T23:24:02+01:00 Download ee4d6aa
Download ff757b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-08T21:34:04+01:00 Download 466232d
Download e5df463 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 14 2018-12-08T06:25:53+01:00 Download d408288
Download 5847524 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-08T03:43:27+01:00 Download 89d962a
Download 414fd9e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-08T02:09:19+01:00 Download fc321db
Download 05b8530 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-07T16:38:43+01:00 Download 910ef60
Download 19cdc95 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-07T08:53:27+01:00 Download 78226ec
Download 84aee68 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-06T09:28:35+01:00 Download 5a8aeba
Download 407269b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 14 2018-12-06T09:09:52+01:00 Download 4e95880
Download 5383add Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 14 2018-12-06T08:25:14+01:00 Download 292207a
Download fa5b064 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 14 2018-12-06T08:14:42+01:00 Download 495f62c
Download 4e95880 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-05T18:46:30+01:00

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

Trying to find witnesses for program (23106d2be7c2d5ee5e241d7f9aabf0dd10692919878117026edb76306f53c494, sv-benchmarks/c/list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i, 23106d2be7c2d5ee5e241d7f9aabf0dd10692919878117026edb76306f53c494
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/23106d2be7c2d5ee5e241d7f9aabf0dd10692919878117026edb76306f53c494.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 (23106d2be7c2d5ee5e241d7f9aabf0dd10692919878117026edb76306f53c494, sv-benchmarks/c/list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i, 23106d2be7c2d5ee5e241d7f9aabf0dd10692919878117026edb76306f53c494
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/23106d2be7c2d5ee5e241d7f9aabf0dd10692919878117026edb76306f53c494.json

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