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/loops/invert_string_false-valid-deref.c
programSHA 160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a
witnessName results-verified/esbmc-kind.2018-12-06_1103.logfiles/sv-comp19_prop-memsafety.invert_string_false-valid-deref.c.files/witness.graphml
witnessSHA c6aceed28ce17ba804acb95dbeb8b48bf74560bfc8d6fe14b4dc9369bf3a9117

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T19:26:48.070380
producer ESBMC 6.0.0 kind
programfile ../../sv-benchmarks/c/loops/invert_string_false-valid-deref.c
programhash 01c8dcbf548ac0eef8cebe655947adbb13d26f9a
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) )
witness-file witnessFileByHash/c6aceed28ce17ba804acb95dbeb8b48bf74560bfc8d6fe14b4dc9369bf3a9117.graphml
witness-sha256 c6aceed28ce17ba804acb95dbeb8b48bf74560bfc8d6fe14b4dc9369bf3a9117
witness-size 4104
witness-type violation_witness

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

Trying to find witnesses for program (160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a, sv-benchmarks/c/loops/invert_string_false-valid-deref.c).

Found 0 witnesses for program sv-benchmarks/c/loops/invert_string_false-valid-deref.c, 160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a.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 (160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a, sv-benchmarks/c/loops/invert_string_false-valid-deref.c).

Found 0 witnesses for program sv-benchmarks/c/loops/invert_string_false-valid-deref.c, 160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a.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 (160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a, sv-benchmarks/c/loops/invert_string_false-valid-deref.c).

Found 0 witnesses for program sv-benchmarks/c/loops/invert_string_false-valid-deref.c, 160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a.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 (160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a, sv-benchmarks/c/loops/invert_string_false-valid-deref.c).

Found 0 witnesses for program sv-benchmarks/c/loops/invert_string_false-valid-deref.c, 160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a.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 (160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a, sv-benchmarks/c/loops/invert_string_false-valid-deref.c).

Found 13 witnesses for program sv-benchmarks/c/loops/invert_string_false-valid-deref.c, 160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2b9b5c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2019-12-02 02:13:56
Download 29394ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 5 2019-12-11T21:09:00+01:00 Download 2b9b5c1
Download 6a93e8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 7 2019-12-08T00:26:09+01:00 Download fdd5135
Download bc3b66b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 7 2019-12-11T21:48:57+01:00 Download 5bc25ca
Download 074091d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 7 2019-12-11T21:44:41+01:00 Download 87e6a1d
Download 3700d69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 7 2019-12-11T20:54:59+01:00 Download 278f1a3
Download 55bd66e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 7 2019-12-07T21:17:13+01:00 Download acfa2b6
Download 6513c49 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 7 2019-12-06T02:38:42+01:00 Download f882d11
Download 84ae189 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 7 2019-11-29T18:36:17+01:00
Download fd0ac55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.9 7 2019-12-08T00:07:42+01:00 Download 53c050f
Download 9cfebd4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.9 7 2019-12-05T20:20:51+01:00 Download 9f4a6ac
Download dfa4d06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.9 7 2019-12-03T08:09:38+01:00 Download 84ae189
Download 87e6a1d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 7 2019-12-01T02:03:41+01:00

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

Trying to find witnesses for program (160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a, sv-benchmarks/c/loops/invert_string_false-valid-deref.c).

Found 15 witnesses for program sv-benchmarks/c/loops/invert_string_false-valid-deref.c, 160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fe80202 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T05:10 CET (sv-comp)
Download 5adbd88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T10:19:11+01:00 Download e2f30c4
Download 6b5da62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:41:10+01:00 Download 95dd051
Download 7ca140a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 7 2018-12-07T22:42:26+01:00
Download 1795cae Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:53:04+01:00 Download 83c692d
Download 1ca0fe8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:23:52+01:00 Download 687e00d
Download e8406ae 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 SMACK 1.9.3 4 2018-12-08T17:34:55
Download 4d6bd4f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T23:43:51+01:00 Download fe80202
Download 93ce597 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T22:10:24+01:00 Download e8406ae
Download 1eeab06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T04:55:30+01:00 Download c6aceed
Download c4f7179 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:40:05+01:00 Download edc2641
Download 71d6236 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-07T01:07:20+01:00 Download 6f017e2
Download 2d91a25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:12:24+01:00 Download 9d41245
Download f47b3e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:00:06+01:00 Download 5138e62
Download cbd585d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T06:24:06+01:00

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

Trying to find witnesses for program (160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a, sv-benchmarks/c/loops/invert_string_false-valid-deref.c).

Found 0 witnesses for program sv-benchmarks/c/loops/invert_string_false-valid-deref.c, 160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a.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 (160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a, sv-benchmarks/c/loops/invert_string_false-valid-deref.c).

Found 0 witnesses for program sv-benchmarks/c/loops/invert_string_false-valid-deref.c, 160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/160e60e7b105ea4b394b7ff1af1478c2fc2bdfab01c677db84a190d24ab9b18a.json

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