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/heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i
programSHA 8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba
witnessName results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-memsafety.sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i.files/witness.graphml
witnessSHA 0b7c7e7a3dd0c9c5ab2cca1d82045d2b86365c2b459885f7672c02fe00187794

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-05T13:49:18.044417
producer DepthK v3.0
programfile /tmp/vcloud-vcloud-master/worker/working_dir_35e36c82-42a5-47cb-8734-810742b2148f/sv-benchmarks/c/heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i
programhash 65263b67fd81174d35f819c28bc33cb1f3e6621f
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/0b7c7e7a3dd0c9c5ab2cca1d82045d2b86365c2b459885f7672c02fe00187794.graphml
witness-sha256 0b7c7e7a3dd0c9c5ab2cca1d82045d2b86365c2b459885f7672c02fe00187794
witness-size 5100
witness-type violation_witness

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

Trying to find witnesses for program (8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba, sv-benchmarks/c/heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i, 8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba.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 (8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba, sv-benchmarks/c/heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i, 8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba.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 (8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba, sv-benchmarks/c/heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i, 8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba.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 (8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba, sv-benchmarks/c/heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i, 8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba.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 (8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba, sv-benchmarks/c/heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i).

Found 22 witnesses for program sv-benchmarks/c/heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i, 8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b88dd04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness Symbiotic 1 2019-12-02 03:27:00
Download 9ab74ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 12 2019-12-11T21:56:30+01:00 Download 2eac00b
Download aa68abc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 13 2019-12-11T21:09:26+01:00 Download b88dd04
Download 6b8ddcd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 12 2019-12-08T00:07:30+01:00 Download 0792343
Download 82d62c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 12 2019-12-03T08:09:53+01:00 Download 2cf1c3a
Download 2cf1c3a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.9 12 2019-11-30T05:12:22+01:00
Download 2eac00b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 12 2019-11-30T20:43:07+01:00
Download ff5d651 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 13:00:09
Download e246305 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 13 2019-12-08T00:06:06+01:00 Download ce186a3
Download d3a3eeb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 13 2019-12-03T08:57:16+01:00 Download 7d2ca79
Download 813ffe2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 15 2019-11-30T03:01:42+01:00
Download 8e42bb1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 15 2019-11-30T21:28:45+01:00
Download 779e307 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 27 2019-12-11T21:43:30+01:00 Download 8e42bb1
Download a986a21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 28 2019-12-11T21:09:06+01:00 Download ff5d651
Download 0c1f17f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 27 2019-12-11T20:54:22+01:00 Download f86f271
Download 80e6a32 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 28 2019-12-11T20:44:27+01:00 Download 1ade5de
Download a384b4c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 27 2019-12-08T01:51:20+01:00 Download 944866e
Download 3e16df5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 27 2019-12-08T00:27:03+01:00 Download e402230
Download 049cea1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 27 2019-12-07T21:16:47+01:00 Download d723c81
Download 34371a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 28 2019-12-06T02:43:45+01:00 Download c78cb02
Download b1d6642 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 27 2019-12-05T20:21:42+01:00 Download 156942b
Download d861f73 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 27 2019-12-03T08:09:39+01:00 Download 813ffe2

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

Trying to find witnesses for program (8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba, sv-benchmarks/c/heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i).

Found 25 witnesses for program sv-benchmarks/c/heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i, 8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 78d658e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness Symbiotic 1 2018-12-08T06:31 CET (sv-comp)
Download 2de7493 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness SMACK 1.9.3 3 2018-12-08T02:39:14
Download 458ed3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-08T23:43:18+01:00 Download 78d658e
Download 3152df7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-08T22:11:24+01:00 Download 2de7493
Download 476950a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-07T09:27:16+01:00 Download 84cbf47
Download 48c8a77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 15 2018-12-06T10:18:24+01:00 Download 0b7c7e7
Download cec5f6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-06T09:48:39+01:00 Download cc9197a
Download cc9197a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-05T12:48:03+01:00
Download d35360a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T16:12 CET (sv-comp)
Download 655e2b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 3 2018-12-08T05:54:32
Download 67ee0ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 15 2018-12-07T09:40:45+01:00
Download 2e6aa37 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-10T10:48:49+01:00 Download cf59d35
Download 4cbbfbe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-08T04:08:00+01:00 Download cf59d35
Download d2299ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 13 2018-12-07T09:25:44+01:00 Download 3e44950
Download eb29818 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 20 2018-12-06T09:10:37+01:00 Download da33900
Download 1a097b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-06T03:02:31+01:00
Download ca18753 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 28 2018-12-10T20:36:49+01:00 Download c7435b3
Download ef0462b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 28 2018-12-09T20:38:32+01:00 Download 0dc9609
Download e6de2ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 29 2018-12-09T18:20:59+01:00 Download 38b8461
Download 10c139f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 28 2018-12-08T23:42:34+01:00 Download d35360a
Download 635bd8f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 28 2018-12-08T22:10:00+01:00 Download 655e2b0
Download bdd7469 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 27 2018-12-08T08:36:34+01:00 Download 67ee0ef
Download 4dd461f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 28 2018-12-08T05:04:43+01:00 Download c60ad61
Download 0fd0a5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 28 2018-12-06T10:13:12+01:00 Download 602c304
Download 07f6700 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 27 2018-12-06T09:48:38+01:00 Download 1a097b9

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

Trying to find witnesses for program (8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba, sv-benchmarks/c/heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i).

Found 15 witnesses for program sv-benchmarks/c/heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i, 8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5e1c3b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T01:39 CET (sv-comp)
Download 3e44950 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness PredatorHP 5 2017-12-01T20:45 CET (sv-comp)
Download 2a0aa6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 3 2017-12-01T21:05 CET (sv-comp)
Download 0b7b14e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Forester 10 2017-12-01T17:55 CET (sv-comp)
Download e2cc9ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 7 2017-12-01T15:04:16.696490
Download 7d2fc94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-01T08:19:56.020670
Download e750d94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-11-30T21:35 CET (sv-comp)
Download 2d1063b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 16 2017-11-30T19:30:25+01:00
Download a5ccc89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 12 2017-11-30T22:00:03+01:00
Download bd3174f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 15 2017-12-02T05:03:53+01:00
Download a5e0c6d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 13 2017-11-30T22:22 CET (sv-comp)
Download a9f83bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 19 2017-12-02T04:20Z
Download 7090cb5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 7 2017-11-30T14:34 CET (sv-comp)
Download 0b23182 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 28 2017-12-01T07:41:09+01:00 26b3fd8
Download d39ddd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 26 2017-11-30T20:20:56+01:00

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

Trying to find witnesses for program (8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba, sv-benchmarks/c/heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i, 8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/8cd1677aec28af36e51443758740a1ca812e34ab0878f4526d2cc8e3dd6e3cba.json

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