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-0232_false-valid-memtrack.i
programSHA f815fca5cb4e3d28ab5a5191e1f8f4aa5035e46e1405135a8e6b714ded762c2f
witnessName results-verified/depthk.2017-12-01_0905.logfiles/sv-comp18.test-0232_false-valid-memtrack.i.files/witness.graphml
witnessSHA b641bf1b969e8c6cce006ab0e0f021afc0b5dc85108f6dc41270049613d76b4c

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-01T09:24 CET (sv-comp)
memoryModel precise
producer ESBMC 3.1
program-sha256 f815fca5cb4e3d28ab5a5191e1f8f4aa5035e46e1405135a8e6b714ded762c2f
programfile /tmp/vcloud-vcloud-master/worker/working_dir_555d13e1-b387-4026-809d-2f0c1de1c3b6/sv-benchmarks/c/memsafety/test-0232_false-valid-memtrack.i
programhash e9df23a7e56f2cc55ab4eafe0f0a27c6f539ef31
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) )
witness-file witnessFileByHash/b641bf1b969e8c6cce006ab0e0f021afc0b5dc85108f6dc41270049613d76b4c.graphml
witness-sha256 b641bf1b969e8c6cce006ab0e0f021afc0b5dc85108f6dc41270049613d76b4c
witness-size 4404
witness-type violation_witness

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

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download dc2d1d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T16:03 CET (sv-comp)
Download 58215c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-10T10:48:51+01:00 Download 4433a0d
Download 6266005 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T23:43:48+01:00 Download dc2d1d4
Download 1a6741a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-07T14:40:27+01:00
Download 0a8806f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-05T19:50:33+01:00
Download 0dace11 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-07T09:26:02+01:00 Download 0c61788
Download 090bb8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:42:41+01:00 Download 7e04008
Download cee8cae Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T22:09:54+01:00 Download 8c583e6
Download 622bd1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T10:20:24+01:00 Download 46d464a
Download 8c583e6 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 3 2018-12-08T16:03:36
Download 9088983 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T04:33:30+01:00 Download 4433a0d
Download 31f52e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-07T01:04:47+01:00 Download cb0a4b0
Download 90523e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T05:05:30+01:00 Download 3b7f2f8
Download a65253f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:19:30+01:00 Download 9413408

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1204bea Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-02T23:47 CET (sv-comp)
Download 0c61788 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness PredatorHP 4 2017-12-01T22:04 CET (sv-comp)
Download 829fe73 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Map2Check 2 2017-12-01T23:36 CET (sv-comp)
Download e42b951 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T11:46:35.840453
Download eebc47f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T23:33:44.118355
Download b641bf1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 3.1 4 2017-12-01T09:24 CET (sv-comp)
Download 1da4aa9 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 11 2017-12-01T08:24 CET (sv-comp)
Download 44730fa 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 2LS 5 2017-12-01T08:19 CET (sv-comp)

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

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

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

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