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/forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i
programSHA e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81
witnessName results-verified/predatorhp.2018-12-07_0408.logfiles/sv-comp19_prop-memsafety.dll-sorted_true-unreach-call_true-valid-memsafety.i.files/witness.graphml
witnessSHA ffb7dcae91ca760f76efbed4be21897c52e08ff1a5e3927969cdf576acc7f298

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-07T07:46 CET (sv-comp)
error-specification-length Key 'specification' longer than 100 characters.
memorymodel precise
producer PredatorHP
programfile ../../sv-benchmarks/c/forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i
programhash 614aedb1ca0b3c75ba5d43ccd1ce8931602b4981
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/ffb7dcae91ca760f76efbed4be21897c52e08ff1a5e3927969cdf576acc7f298.graphml
witness-sha256 ffb7dcae91ca760f76efbed4be21897c52e08ff1a5e3927969cdf576acc7f298
witness-size 3652
witness-type correctness_witness

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

Trying to find witnesses for program (e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81, sv-benchmarks/c/forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i, e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81.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 (e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81, sv-benchmarks/c/forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i, e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81.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 (e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81, sv-benchmarks/c/forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i, e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81.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 (e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81, sv-benchmarks/c/forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i, e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81.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 (e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81, sv-benchmarks/c/forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i).

Found 5 witnesses for program sv-benchmarks/c/forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i, e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ef1bab6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 16 2019-11-30T14:20:53+01:00
Download 881182e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 16 2019-12-01T00:41:49+01:00
Download 014da3d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-12-07T23:47:03+01:00 Download 6ebe44a
Download b453ab3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 16 2019-11-30T16:40:21+01:00 Download 634dea7
Download 634dea7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 17 2019-11-29T14:58:48+01:00

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

Trying to find witnesses for program (e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81, sv-benchmarks/c/forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i).

Found 6 witnesses for program sv-benchmarks/c/forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i, e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 639cceb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 16 2018-12-07T06:51:05+01:00
Download 8bb1994 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T10:24:59
Download 888b858 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 17 2018-12-08T04:03:16+01:00
Download 1d2e8ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-08T21:44:19+01:00 Download 8bb1994
Download 5f839de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 17 2018-12-08T06:07:09+01:00 Download 888b858
Download 971293e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 16 2018-12-07T08:16:03+01:00 Download 3de5230

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

Trying to find witnesses for program (e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81, sv-benchmarks/c/forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i).

Found 8 witnesses for program sv-benchmarks/c/forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i, e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download faaf09a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Forester 98 2017-12-01T19:34 CET (sv-comp)
Download 8526744 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 7 2017-12-01T03:04:20+01:00
Download 3de5230 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness PredatorHP 4 2017-12-01T20:30 CET (sv-comp)
Download b0339a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Forester 98 2017-12-01T18:02 CET (sv-comp)
Download c99d061 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 16 2017-12-01T21:19:25+01:00 6f35f84
Download 4f93c2e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 16 2017-12-01T18:48:07+01:00 aec54c3
Download 6ac40fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 16 2017-12-01T07:09:32+01:00 d7dda66
Download 50c4747 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 27 2017-12-01T01:31:08+01:00

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

Trying to find witnesses for program (e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81, sv-benchmarks/c/forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i, e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/e47c8b93ddf710e18d3897bf4c5ffd7742657ca169a7f697c50b16fbb5f95a81.json

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