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-free.i
programSHA 47c40f772f7d29009c4621b41b6f87e9da4b0174af4a8b9de4bccc3eaa01aad8
witnessName results-verified/symbiotic.2017-12-02_2308.logfiles/sv-comp18.test-0232_false-valid-free.i.files/witness.graphml
witnessSHA 40dedc89b338f8f806466ebe077985b3784ac5935cfa8bd98d74fcfcfc033148

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-02T23:18 CET (sv-comp)
producer Symbiotic
program-sha256 47c40f772f7d29009c4621b41b6f87e9da4b0174af4a8b9de4bccc3eaa01aad8
programfile /tmp/vcloud-vcloud-master/worker/working_dir_8f977b60-bcf0-4448-ab88-05123705fdec/sv-benchmarks/c/memsafety/test-0232_false-valid-free.i
programhash 1197d671a588cd166018a116686924380f8bf0f7
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-memtrack) )
witness-file witnessFileByHash/40dedc89b338f8f806466ebe077985b3784ac5935cfa8bd98d74fcfcfc033148.graphml
witness-sha256 40dedc89b338f8f806466ebe077985b3784ac5935cfa8bd98d74fcfcfc033148
witness-size 921
witness-type violation_witness

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

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 820b69d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T09:55 CET (sv-comp)
Download 1b0594e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-10T10:48:45+01:00 Download 0f7701a
Download 47088e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T22:11:07+01:00 Download b97e73c
Download cdbe6f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T04:35:25+01:00 Download 0f7701a
Download 366db73 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T10:17:47+01:00 Download 7159837
Download 9a4c16f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 7 2018-12-08T00:36:56+01:00
Download 88edbe4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-09T20:34:06+01:00 Download 2a4567e
Download 2e9214b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-07T09:17:11+01:00 Download 2d466d3
Download fe1d0f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T07:47:50+01:00
Download b97e73c 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-08T05:52:55
Download 6d9b6e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T23:43:26+01:00 Download 820b69d
Download 6398d5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T05:06:17+01:00 Download 40f4da0
Download f0dfd5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:17:21+01:00 Download ef62da4

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 40dedc8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-02T23:18 CET (sv-comp)
Download 029a857 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 kind 5 2017-12-02T11:05:56.495934
Download d7595b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-01T23:27:18.246604
Download b952fc2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 3.1 5 2017-12-01T09:36 CET (sv-comp)
Download 2d466d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness PredatorHP 5 2017-12-01T22:16 CET (sv-comp)
Download 86441a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness Map2Check 3 2017-12-01T23:43 CET (sv-comp)
Download f4c4022 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 23 2017-12-01T08:30 CET (sv-comp)

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

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

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

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