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/ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i
programSHA c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7
witnessName results-verified/ukojak.2017-12-02_0233.logfiles/sv-comp18.ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i.files/witness.graphml
witnessSHA 707e63c10dbf627b6b680ed8ca4ef4b7eb8d2771d287a8fc0ff57506356b55f0

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/707e63c10dbf627b6b680ed8ca4ef4b7eb8d2771d287a8fc0ff57506356b55f0.json

Key Value
architecture 32bit
creationtime 2017-12-02T14:04Z
producer Kojak
program-sha256 c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7
programfile /tmp/vcloud-vcloud-master/worker/working_dir_2234637c-af2a-4a7e-836d-4f425afc0356/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i
programhash 1e57fc2102c49e62bdc512891f0be08939a537f0
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/707e63c10dbf627b6b680ed8ca4ef4b7eb8d2771d287a8fc0ff57506356b55f0.graphml
witness-sha256 707e63c10dbf627b6b680ed8ca4ef4b7eb8d2771d287a8fc0ff57506356b55f0
witness-size 212709
witness-type correctness_witness

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

Trying to find witnesses for program (c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7, sv-benchmarks/c/ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i, c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7.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 (c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7, sv-benchmarks/c/ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i, c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7.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 (c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7, sv-benchmarks/c/ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i, c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7.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 (c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7, sv-benchmarks/c/ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i, c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7.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 (c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7, sv-benchmarks/c/ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i, c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7.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 (c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7, sv-benchmarks/c/ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i, c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7.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 '18

Trying to find witnesses for program (c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7, sv-benchmarks/c/ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i).

Found 27 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i, c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3e60963 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-02T23:32 CET (sv-comp)
Download 74cb0fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness PredatorHP 6 2017-12-01T21:54 CET (sv-comp)
Download 02d1670 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Map2Check 3 2017-12-01T23:53 CET (sv-comp)
Download e8e1aef Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CBMC 43 2017-12-01T08:21 CET (sv-comp)
Download cfd8ea2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.6.1-svn 26773 39 2017-12-01T08:29:25+01:00
Download 08aa630 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T23:11 CET (sv-comp)
Download aa63e26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 221 2017-12-03T05:10Z
Download 16e965c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T11:17 CET (sv-comp)
Download 707e63c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 213 2017-12-02T14:04Z
Download ccbd9c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T21:26:52.347458
Download 9c80752 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 144 2017-12-03T00:46:05+01:00
Download 2888b9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-03T06:51:04+01:00 1f706c3
Download 01ad0d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-03T04:04:04+01:00 7fa0d0d
Download 89b228e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-03T02:59:16+01:00 b42a051
Download 677a24a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-03T00:47:37+01:00 13c9d78
Download 3d822cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-02T20:05:38+01:00 f6e2634
Download dcce669 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-02T15:02:23+01:00 9ae8edc
Download 060139c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-02T07:08:21+01:00 fa9575f
Download 7155d34 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-02T00:13:37+01:00 e90e043
Download 872fca7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-01T06:45:12+01:00 5ab0b7c
Download b9c5386 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-01T06:10:10+01:00 848b752
Download bd8e875 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-01T04:35:22+01:00 716249b
Download 078e89e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 125 2017-12-01T03:54:44+01:00
Download 2d5ac92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 5 2017-11-30T18:54:15+01:00
Download 3007428 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 144 2017-11-30T20:58:05+01:00
Download 4187f33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 4 2017-12-02T09:07:28+01:00
Download fd16721 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 221 2017-12-02T19:01Z

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

Trying to find witnesses for program (c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7, sv-benchmarks/c/ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i, c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/c5b6d0e8e6d029a340cb6cb12dbdfef6d78783d42c1f1cf3cc5973a67c0a99a7.json

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