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/busybox-1.22.0/basename_false-valid-deref.i
programSHA 5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4
witnessName results-verified/esbmc-kind.2018-12-06_1103.logfiles/sv-comp19_prop-memsafety.basename_false-valid-deref.i.files/witness.graphml
witnessSHA ce146fa01e8999b59bb90197211faa3fe3480c5583be07002115808b949ccd57

Information about the Witness from Competition Database

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

Key Value
architecture 64bit
creationtime 2018-12-07T16:38:07.306547
producer ESBMC 6.0.0 kind
programfile ../../sv-benchmarks/c/busybox-1.22.0/basename_false-valid-deref.i
programhash 655151af4c76f34ceb25a5357f50e8b2fc857fa3
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) )
witness-file witnessFileByHash/ce146fa01e8999b59bb90197211faa3fe3480c5583be07002115808b949ccd57.graphml
witness-sha256 ce146fa01e8999b59bb90197211faa3fe3480c5583be07002115808b949ccd57
witness-size 9419
witness-type violation_witness

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

Trying to find witnesses for program (5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4, sv-benchmarks/c/busybox-1.22.0/basename_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/busybox-1.22.0/basename_false-valid-deref.i, 5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4.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 (5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4, sv-benchmarks/c/busybox-1.22.0/basename_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/busybox-1.22.0/basename_false-valid-deref.i, 5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4.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 (5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4, sv-benchmarks/c/busybox-1.22.0/basename_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/busybox-1.22.0/basename_false-valid-deref.i, 5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4.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 (5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4, sv-benchmarks/c/busybox-1.22.0/basename_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/busybox-1.22.0/basename_false-valid-deref.i, 5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4.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 (5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4, sv-benchmarks/c/busybox-1.22.0/basename_false-valid-deref.i).

Found 6 witnesses for program sv-benchmarks/c/busybox-1.22.0/basename_false-valid-deref.i, 5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 132e820 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 32 2019-12-11T21:59:53+01:00 Download 397eee3
Download 0260f44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 32 2019-12-05T20:21:21+01:00 Download 64b66f6
Download e3bde37 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 32 2019-12-03T08:08:28+01:00 Download b06f54e
Download b06f54e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 31 2019-11-30T14:38:16+01:00
Download 397eee3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 31 2019-11-30T20:51:46+01:00
Download 86e9f1f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.9 32 2019-12-11T21:09:23+01:00 Download cc58b96

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

Trying to find witnesses for program (5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4, sv-benchmarks/c/busybox-1.22.0/basename_false-valid-deref.i).

Found 6 witnesses for program sv-benchmarks/c/busybox-1.22.0/basename_false-valid-deref.i, 5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d07ee31 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2018-12-08T02:33 CET (sv-comp)
Download c07ee88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 31 2018-12-07T21:01:40+01:00
Download 80ed274 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 32 2018-12-08T05:01:05+01:00 Download ce146fa
Download a67b9ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 31 2018-12-05T21:39:51+01:00
Download 98c8130 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.7-svn 29852 32 2018-12-06T09:20:16+01:00 Download 17a3470
Download eebe9f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 33 2018-12-08T23:42:08+01:00 Download d07ee31

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

Trying to find witnesses for program (5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4, sv-benchmarks/c/busybox-1.22.0/basename_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/busybox-1.22.0/basename_false-valid-deref.i, 5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4.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 (5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4, sv-benchmarks/c/busybox-1.22.0/basename_false-valid-deref.i).

Found 0 witnesses for program sv-benchmarks/c/busybox-1.22.0/basename_false-valid-deref.i, 5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/5807edd976795de0fc9b4c59731b29e970a3a7668b3fa1e868905f48e9ac81c4.json

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