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-properties/list_search_false-unreach-call_false-valid-memcleanup.i
programSHA 5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c
witnessName results-verified/2ls.2018-12-04_2244.logfiles/sv-comp19_prop-reachsafety.list_search_false-unreach-call_false-valid-memcleanup.i.files/witness.graphml
witnessSHA 86e12720de1cdef42433869838ef25c051f5bbdb4b8b2a01698a502b1956431a

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-05T18:19 CET (sv-comp)
producer 2LS
programfile ../../sv-benchmarks/c/list-properties/list_search_false-unreach-call_false-valid-memcleanup.i
programhash 9fdfa874c4a41b156e998d9e6fe5a8270aecd034
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/86e12720de1cdef42433869838ef25c051f5bbdb4b8b2a01698a502b1956431a.graphml
witness-sha256 86e12720de1cdef42433869838ef25c051f5bbdb4b8b2a01698a502b1956431a
witness-size 8502
witness-type violation_witness

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

Trying to find witnesses for program (5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c, sv-benchmarks/c/list-properties/list_search_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/list-properties/list_search_false-unreach-call_false-valid-memcleanup.i, 5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c.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 (5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c, sv-benchmarks/c/list-properties/list_search_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/list-properties/list_search_false-unreach-call_false-valid-memcleanup.i, 5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c.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 (5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c, sv-benchmarks/c/list-properties/list_search_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/list-properties/list_search_false-unreach-call_false-valid-memcleanup.i, 5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c.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 (5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c, sv-benchmarks/c/list-properties/list_search_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/list-properties/list_search_false-unreach-call_false-valid-memcleanup.i, 5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c.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 (5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c, sv-benchmarks/c/list-properties/list_search_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/list-properties/list_search_false-unreach-call_false-valid-memcleanup.i, 5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c.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 (5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c, sv-benchmarks/c/list-properties/list_search_false-unreach-call_false-valid-memcleanup.i).

Found 34 witnesses for program sv-benchmarks/c/list-properties/list_search_false-unreach-call_false-valid-memcleanup.i, 5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c0af3fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness Symbiotic 1 2018-12-08T07:19 CET (sv-comp)
Download 009e181 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness SMACK 1.9.3 3 2018-12-08T10:44:36
Download 796b008 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-08T23:44:50+01:00 Download c0af3fe
Download 9d444a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-08T22:10:27+01:00 Download 009e181
Download 7f8f17c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-07T09:28:03+01:00 Download b841179
Download e6cd646 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-06T10:19:05+01:00 Download df9e52d
Download 7be3ae8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-06T09:48:16+01:00 Download f3a2377
Download f3a2377 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 20 2018-12-05T16:43:40+01:00
Download d98a1f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:40:29+01:00 Download a35c88f
Download 4e8583a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:18:28+01:00 Download 52356dc
Download 1c6bf94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T01:08 CET (sv-comp)
Download 845bc9e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 3 2018-12-08T08:29:30
Download 2eeb534 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 14 2018-12-07T11:00 CET (sv-comp)
Download 4a128bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 15 2018-12-10T18:41:43+01:00
Download ca80f07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 20 2018-12-08T03:43:02+01:00
Download 72e472a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-09T20:53:25+01:00 Download 788df34
Download 15ff03d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-09T20:37:58+01:00 Download 1302506
Download 1c9d03e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 20 2018-12-08T08:03:43+01:00 Download ca80f07
Download 0f487cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 20 2018-12-08T05:05:58+01:00 Download 322d052
Download 1615f9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-07T17:43:12+01:00 Download 2eeb534
Download 8da5f43 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 20 2018-12-06T10:14:57+01:00 Download 1547821
Download 99b691f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 20 2018-12-06T09:49:16+01:00 Download 7ef28d3
Download 0433645 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-06T09:17:07+01:00 Download 435b8fa
Download 0670b3d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 21 2018-12-06T09:09:22+01:00 Download 05b0a69
Download 7ef28d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 20 2018-12-06T02:41:57+01:00
Download 9c4b366 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-10T20:37:06+01:00 Download 4a128bb
Download 44c18fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-10T10:48:44+01:00 Download 8c2089b
Download 9b7de50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-09T18:20:30+01:00 Download 56c3d5a
Download 0eb3ef7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T23:44:42+01:00 Download 1c6bf94
Download 8527440 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T22:10:44+01:00 Download 845bc9e
Download c2b314a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T03:56:04+01:00 Download 8c2089b
Download fa90c04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-07T09:27:23+01:00 Download f132a50
Download 8db23af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-07T01:21:04+01:00 Download 222e987
Download 2241e6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:40:28+01:00 Download 86e1272

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

Trying to find witnesses for program (5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c, sv-benchmarks/c/list-properties/list_search_false-unreach-call_false-valid-memcleanup.i).

Found 16 witnesses for program sv-benchmarks/c/list-properties/list_search_false-unreach-call_false-valid-memcleanup.i, 5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 37ecb45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 23 2017-12-02T18:50Z
Download ebc4764 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T01:00 CET (sv-comp)
Download f132a50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness PredatorHP 5 2017-12-01T20:48 CET (sv-comp)
Download 49e6ce6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 6 2017-12-01T21:36 CET (sv-comp)
Download fdb5a73 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Forester 11 2017-12-01T18:07 CET (sv-comp)
Download ac5ab6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 6 2017-12-01T14:01:05.553614
Download 311b94a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 6 2017-12-01T09:08:37.478069
Download fb43604 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 6 2017-11-30T22:05 CET (sv-comp)
Download 06f08c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 19 2017-11-30T11:24:18+01:00
Download 0393ba9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 9 2017-12-01T02:17:33+01:00
Download ff95ddd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 15 2017-12-02T13:51:15+01:00
Download 3844cb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 15 2017-11-30T13:51 CET (sv-comp)
Download 4e04222 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 23 2017-12-02T17:40Z
Download 86e1272 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 9 2017-11-30T19:16 CET (sv-comp)
Download d3e0d5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 10 2017-12-01T07:40:44+01:00 8737f9b
Download c59788d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 13 2017-11-30T16:15:54+01:00

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

Trying to find witnesses for program (5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c, sv-benchmarks/c/list-properties/list_search_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/list-properties/list_search_false-unreach-call_false-valid-memcleanup.i, 5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/5f228af9cf7c06768847be979306689710f5ce6da310c1b6d69433b6a9d7ce2c.json

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