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-verified/cpa-seq.2018-12-05_0546.logfiles/sv-comp19_prop-memsafety.test-0102_false-valid-memtrack.i.files/witness.graphml
witnessSHA 63820caac879a2901e09a72fac14076485990b03e19f743ee8bf5831d0dc48ea

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-05T13:34:18+01:00
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/63820caac879a2901e09a72fac14076485990b03e19f743ee8bf5831d0dc48ea.graphml
witness-sha256 63820caac879a2901e09a72fac14076485990b03e19f743ee8bf5831d0dc48ea
witness-size 12340
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