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/memsafety/test-0102_false-valid-memtrack.i
programSHA bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2
witnessName results-validated/cpa-seq-validate-violation-witnesses-depthk.2018-12-06_1002.logfiles/sv-comp19_prop-memsafety.test-0102_false-valid-memtrack.i.files/witness.graphml
witnessSHA d1bf787a66604a88ecd60a2e46a6b1cb1c0dbf5491392ca01c8b46c2c43b9865

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T10:19:19+01:00
inputwitnesshash c406ca39adb0170332c2f1f319bb1a33813729355087d9420a03c98c70681c8d
producer CPAchecker 1.7-svn 29852
program-sha256 bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2
programfile ../../sv-benchmarks/c/memsafety/test-0102_false-valid-memtrack.i
programhash bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-memtrack) )
witness-file witnessFileByHash/d1bf787a66604a88ecd60a2e46a6b1cb1c0dbf5491392ca01c8b46c2c43b9865.graphml
witness-sha256 d1bf787a66604a88ecd60a2e46a6b1cb1c0dbf5491392ca01c8b46c2c43b9865
witness-size 12443
witness-type correctness_witness

This witness was created for this program (cf. table above, bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2).

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

Trying to find witnesses for program (bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2, sv-benchmarks/c/memsafety/test-0102_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0102_false-valid-memtrack.i, bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2.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 (bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2, sv-benchmarks/c/memsafety/test-0102_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0102_false-valid-memtrack.i, bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2.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 (bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2, sv-benchmarks/c/memsafety/test-0102_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0102_false-valid-memtrack.i, bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2.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 (bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2, sv-benchmarks/c/memsafety/test-0102_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0102_false-valid-memtrack.i, bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2.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 (bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2, sv-benchmarks/c/memsafety/test-0102_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0102_false-valid-memtrack.i, bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2.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 (bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2, sv-benchmarks/c/memsafety/test-0102_false-valid-memtrack.i).

Found 9 witnesses for program sv-benchmarks/c/memsafety/test-0102_false-valid-memtrack.i, bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5827c45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T03:27 CET (sv-comp)
Download ce05754 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 17 2018-12-08T23:42:44+01:00 Download 5827c45
Download 7d845cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 12 2018-12-08T02:08:50+01:00
Download d1bf787 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-06T10:19:19+01:00 Download c406ca3
Download 63820ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-05T13:34:18+01:00
Download 183a0a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 17 2018-12-07T09:24:04+01:00 Download 4ff5107
Download 549dfaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 18 2018-12-07T01:14:52+01:00 Download 495279e
Download afcbdba Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-10T10:49:49+01:00 Download 8afadb6
Download 3de7880 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-08T04:59:46+01:00 Download 4693ab6

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

Trying to find witnesses for program (bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2, sv-benchmarks/c/memsafety/test-0102_false-valid-memtrack.i).

Found 7 witnesses for program sv-benchmarks/c/memsafety/test-0102_false-valid-memtrack.i, bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 43d0ecc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-03T00:28 CET (sv-comp)
Download 4ff5107 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness PredatorHP 6 2017-12-01T22:01 CET (sv-comp)
Download 1eb7cf3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Map2Check 3 2017-12-01T23:26 CET (sv-comp)
Download c1b69a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 kind 8 2017-12-02T11:17:30.797967
Download 912a066 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 incr 16 2017-12-01T23:13:26.014478
Download c7e86af Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 3.1 5 2017-12-01T09:35 CET (sv-comp)
Download 3dfb7d9 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 38 2017-12-01T08:21 CET (sv-comp)

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

Trying to find witnesses for program (bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2, sv-benchmarks/c/memsafety/test-0102_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/memsafety/test-0102_false-valid-memtrack.i, bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/bee1d9cb23a1858cdadee487aabd2128750878c38f6807b7f9f2b4022b0122b2.json

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