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_true-unreach-call_false-valid-memcleanup.i
programSHA a3fa57ab72bd37f0f8e4617e59c44eae2fe42aba95612055b86db99c388a382e
witnessName results-validated/cpa-seq-validate-correctness-witnesses-cpa-seq.2018-12-06_0837.logfiles/sv-comp19_prop-reachsafety.list_search_true-unreach-call_false-valid-memcleanup.i.files/witness.graphml
witnessSHA aa502e37e16f0f3734430be88dae72e0be93fc1cfa24eb07256cd3e272fc7278

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T08:45:48+01:00
inputwitnesshash d21b568d3658e402a05f8702219764f4d8825e23820d90de74d5bf21c0a071f6
producer CPAchecker 1.7-svn 29852
program-sha256 a3fa57ab72bd37f0f8e4617e59c44eae2fe42aba95612055b86db99c388a382e
programfile ../../sv-benchmarks/c/list-properties/list_search_true-unreach-call_false-valid-memcleanup.i
programhash a3fa57ab72bd37f0f8e4617e59c44eae2fe42aba95612055b86db99c388a382e
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/aa502e37e16f0f3734430be88dae72e0be93fc1cfa24eb07256cd3e272fc7278.graphml
witness-sha256 aa502e37e16f0f3734430be88dae72e0be93fc1cfa24eb07256cd3e272fc7278
witness-size 12916
witness-type correctness_witness

This witness was created for this program (cf. table above, a3fa57ab72bd37f0f8e4617e59c44eae2fe42aba95612055b86db99c388a382e).

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

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 54ce4c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness Symbiotic 1 2018-12-08T03:52 CET (sv-comp)
Download d54c537 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness SMACK 1.9.3 3 2018-12-08T05:03:40
Download 07157c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 24 2018-12-08T23:42:23+01:00 Download 54ce4c0
Download 1e60598 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 24 2018-12-08T22:08:18+01:00 Download d54c537
Download ecc33dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 24 2018-12-06T09:48:26+01:00 Download 63fd61c
Download c9458c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 25 2018-12-06T09:42:02+01:00 Download bac366b
Download 63fd61c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 33 2018-12-05T23:13:36+01:00
Download 0ac3a7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-07T09:15:16+01:00 Download c243a65
Download 3dcda84 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-06T09:16:56+01:00 Download a83bbee
Download 91b9932 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-06T09:00:27+01:00 Download af76b02
Download 6a929d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T07:25 CET (sv-comp)
Download b4455f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T00:11:29
Download b7c1073 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T10:06 CET (sv-comp)
Download 757a530 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 13 2018-12-10T18:07:53+01:00
Download 4b64d7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 13 2018-12-08T04:21:39+01:00
Download 384acff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-10T20:05:43+01:00 Download 757a530
Download 2579622 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-10T10:31:47+01:00 Download aa3bc8b
Download 4bc5191 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-09T20:03:44+01:00 Download d591435
Download cb07786 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-08T23:11:28+01:00 Download 6a929d8
Download 12d3423 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-08T21:43:06+01:00 Download b4455f9
Download 0ab13ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-08T07:12:11+01:00 Download 4b64d7b
Download 12fbfcc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-08T03:45:39+01:00 Download c1cc45a
Download e0c71b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-08T02:44:39+01:00 Download aa3bc8b
Download c236edb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-07T16:39:30+01:00 Download b7c1073
Download 3a98b45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-07T08:52:32+01:00 Download 4a65301
Download cca58f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-06T09:28:26+01:00 Download fab497d
Download aa502e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-06T08:45:48+01:00 Download d21b568
Download 69aacd7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-06T08:29:56+01:00 Download cbf1b0f
Download 1093bd9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-06T08:11:52+01:00 Download 922a8d4
Download d21b568 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-05T14:40:49+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 82905be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 10 2017-11-30T15:32:55+01:00
Download eb26de6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T07:37 CET (sv-comp)
Download 4a65301 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness PredatorHP 4 2017-12-01T20:52 CET (sv-comp)
Download 0b1a549 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 8 2017-12-01T21:33 CET (sv-comp)
Download c91cbd0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Forester 31 2017-12-01T18:11 CET (sv-comp)
Download e6cf6e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T13:03:05.531868
Download 4d802c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T18:29:33.711610
Download f510547 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 19 2017-11-30T18:06 CET (sv-comp)
Download 8a1da98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 13 2017-12-02T22:53:38+01:00
Download 0379d10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-03T04:10:08+01:00 33379ef
Download e580759 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-03T01:26:03+01:00 39dbbb7
Download 63256b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-02T20:47:48+01:00 52b4718
Download 04c7833 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-02T15:21:02+01:00 34a27a4
Download 088eb4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-02T08:39:09+01:00 9055217
Download 6bb72a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-01T22:33:06+01:00 c49cee2
Download eb438ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-01T22:16:03+01:00 4b38cf6
Download 9e34870 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-01T21:04:45+01:00 8b06211
Download 4435ea5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-01T18:33:48+01:00 4904125
Download dbe238e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-01T08:13:38+01:00 18d4808
Download 48accc7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-01T06:25:31+01:00 c48e57b
Download a9197a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-01T06:24:39+01:00 498fca3
Download 9231577 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-01T05:31:01+01:00 32a6a71
Download b5d8d59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-11-30T13:28:01+01:00
Download 64920da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 15 2017-11-30T18:19:03+01:00
Download 144969b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 9 2017-12-02T04:15:31+01:00
Download 7e9e459 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 35 2017-11-30T18:51 CET (sv-comp)
Download 0ae834d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 20 2017-12-02T15:43Z
Download 1182e69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 65 2017-12-01T03:52 CET (sv-comp)

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

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

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

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