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/sll_length_check_true-unreach-call_true-valid-memsafety.i
programSHA 04a3ed215fcb65532398032e6c27820230198c232758062c7e5a54b91fa9cdb7
witnessName results-verified/cbmc.2018-12-04_2248.logfiles/sv-comp19_prop-memsafety.sll_length_check_true-unreach-call_true-valid-memsafety.i.files/witness.graphml
witnessSHA 4f0f8d049660dbbca2d35ce0cace9430f73f7b4aef3c2c46d91271611904be48

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T00:42 CET (sv-comp)
error-specification-length Key 'specification' longer than 100 characters.
producer CBMC
programfile ../../sv-benchmarks/c/list-ext3-properties/sll_length_check_true-unreach-call_true-valid-memsafety.i
programhash 13de6e88afef243c8793160461f39a44fcce6b24
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/4f0f8d049660dbbca2d35ce0cace9430f73f7b4aef3c2c46d91271611904be48.graphml
witness-sha256 4f0f8d049660dbbca2d35ce0cace9430f73f7b4aef3c2c46d91271611904be48
witness-size 498023
witness-type correctness_witness

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 05a4a9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 11 2019-11-29T14:28:07+01:00
Download 43fd334 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 11 2019-11-30T23:55:32+01:00
Download e9b25ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 11 2019-12-11T20:34:43+01:00 Download 5502d65
Download 2f0640f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 11 2019-12-11T20:33:26+01:00 Download 9184e48
Download 79658a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 11 2019-12-08T00:51:40+01:00 Download 1389c81
Download 7b2717f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 11 2019-12-08T00:00:02+01:00 Download 355acef
Download 5d33b7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 11 2019-12-06T02:32:12+01:00 Download 5200710
Download 39c0aaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 11 2019-11-30T19:55:33+01:00 Download 346a0ef
Download e69edef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 11 2019-11-30T16:58:55+01:00 Download 1d5c8ad
Download 1d5c8ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 85 2019-11-30T01:24:06+01:00
Download 1389c81 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 24 2019-12-07T13:25:50+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e75fccb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2018-12-08T13:41 CET (sv-comp)
Download 24dde3e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 11 2018-12-07T01:32:46+01:00
Download 9d3e05a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-05T19:57:15+01:00
Download 650600e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T05:37 CET (sv-comp)
Download 3290744 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-07T20:24:54
Download 2579f7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 14 2018-12-10T19:10:44+01:00
Download 17f1ad4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 87 2018-12-07T06:52:15+01:00
Download 67b1dbf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-10T19:51:18+01:00 Download 2579f7f
Download 564f168 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-10T10:45:35+01:00 Download 2d68413
Download 3b79e31 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-08T23:38:20+01:00 Download 650600e
Download b65f653 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-08T21:52:11+01:00 Download 3290744
Download 5d1ae8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-08T06:06:24+01:00 Download 17f1ad4
Download 27d21f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-08T03:35:20+01:00 Download 9536178
Download 372ed19 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-08T02:23:26+01:00 Download 2d68413
Download 8283d1d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-07T09:06:59+01:00 Download 12013d9
Download 5d56415 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 11 2018-12-06T09:42:35+01:00 Download 4cb035b
Download aa5dccf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-06T09:00:09+01:00 Download fd74c15
Download fd74c15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 101 2018-12-05T09:57:33+01:00

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

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

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

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

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