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/list-properties/list_false-unreach-call_false-valid-memcleanup.i
programSHA e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3
witnessName results-verified/ukojak.2018-12-08_1104.logfiles/sv-comp19_prop-reachsafety.list_false-unreach-call_false-valid-memcleanup.i.files/witness.graphml
witnessSHA ad4837f8247cb04860ffd935c662158bd7af7192e61854c8ce1bcbf613d8fd3e

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-09T09:45Z
producer Kojak
programfile /tmp/vcloud-vcloud-master/worker/working_dir_d4e8a1ed-eafa-4c40-8f89-daf94d2c6762/sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i
programhash 59941807ee61f14408f8cb6acb0590ac0607fc0d
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/ad4837f8247cb04860ffd935c662158bd7af7192e61854c8ce1bcbf613d8fd3e.graphml
witness-sha256 ad4837f8247cb04860ffd935c662158bd7af7192e61854c8ce1bcbf613d8fd3e
witness-size 12669
witness-type violation_witness

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

Trying to find witnesses for program (e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3, sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i, e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3.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 (e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3, sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i, e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3.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 (e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3, sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i, e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3.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 (e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3, sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i, e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3.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 (e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3, sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i, e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3.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 (e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3, sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i).

Found 33 witnesses for program sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i, e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 67100eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness Symbiotic 1 2018-12-08T01:54 CET (sv-comp)
Download b85bfc2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness SMACK 1.9.3 3 2018-12-07T20:44:43
Download 8986514 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-08T23:42:33+01:00 Download 67100eb
Download 831bdf8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-08T22:07:36+01:00 Download b85bfc2
Download 534cebc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-06T10:10:28+01:00 Download da3fc65
Download 5a36e71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 10 2018-12-06T09:48:14+01:00 Download b093068
Download b093068 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 12 2018-12-06T06:58:10+01:00
Download 4b3197c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-09T20:54:12+01:00 Download 7464bcd
Download 6ac192e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-09T20:40:06+01:00 Download 10c5e54
Download 704d1a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-09T20:27:25+01:00 Download a46db28
Download 0e32e01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-07T09:14:00+01:00 Download 05781e0
Download 32d7b1b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:43:53+01:00 Download ffd4926
Download f02fe59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:20:30+01:00 Download 1303aa6
Download 9b30d37 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T11:38 CET (sv-comp)
Download 1233edb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 3 2018-12-08T02:11:40
Download 64c59a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 11 2018-12-07T10:02:54+01:00
Download 66d8f2e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-09T20:53:10+01:00 Download d47db50
Download 35fc098 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-09T20:37:11+01:00 Download 6dc3cdf
Download c3348a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-09T20:18:39+01:00 Download ad4837f
Download 7e9f3ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-08T05:02:56+01:00 Download f28f062
Download fa485de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-06T10:18:23+01:00 Download e3aa8c3
Download 081fbf9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-06T09:20:06+01:00 Download 7ba4fcf
Download 7e94a06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-05T20:24:20+01:00
Download 1ab04e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-10T20:36:26+01:00 Download 1706ab4
Download c6d2391 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-10T10:48:51+01:00 Download e2d80ea
Download cda5a8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-09T18:22:35+01:00 Download c816a25
Download b6432a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T23:43:47+01:00 Download 9b30d37
Download f2f5ad7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T22:11:15+01:00 Download 1233edb
Download b3fd022 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T09:05:56+01:00 Download 64c59a3
Download 3da8dd0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T03:51:42+01:00 Download e2d80ea
Download dacfcfb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-07T09:30:06+01:00 Download 30402f1
Download 1e08850 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-07T01:09:53+01:00 Download 685b0c2
Download 5637826 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:48:41+01:00 Download 7e94a06

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

Trying to find witnesses for program (e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3, sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i, e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3.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 (e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3, sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i).

Found 0 witnesses for program sv-benchmarks/c/list-properties/list_false-unreach-call_false-valid-memcleanup.i, e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/e81ec3318649d2efdcdf2d70fba9ff8697474aaa30098d43c7b9cf85811c31b3.json

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