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-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i
programSHA ccdb3117b6c3e0771df9b385db7fb1f05f5a559f190583f324aa75f9d6f30cb1
witnessName results-verified/utaipan.2018-12-08_1419.logfiles/sv-comp19_prop-memsafety.simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i.files/witness.graphml
witnessSHA 67d04ff28b54f56a2a98922a8855ec3ed724fc70fee1d1df104fff767d5c1f1a

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-09T03:54Z
producer Taipan
programfile /tmp/vcloud-vcloud-master/worker/working_dir_f4b5fba1-b7b9-4a18-a64c-b1d7dd6f22c7/sv-benchmarks/c/list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i
programhash 9becd42a466bdbd2531661a22b57e70854c9d9ea
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-memcleanup) )
witness-file witnessFileByHash/67d04ff28b54f56a2a98922a8855ec3ed724fc70fee1d1df104fff767d5c1f1a.graphml
witness-sha256 67d04ff28b54f56a2a98922a8855ec3ed724fc70fee1d1df104fff767d5c1f1a
witness-size 16724
witness-type correctness_witness

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

Trying to find witnesses for program (ccdb3117b6c3e0771df9b385db7fb1f05f5a559f190583f324aa75f9d6f30cb1, sv-benchmarks/c/list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i).

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

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

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

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

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

Found 37 witnesses for program sv-benchmarks/c/list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i, ccdb3117b6c3e0771df9b385db7fb1f05f5a559f190583f324aa75f9d6f30cb1
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ccdb3117b6c3e0771df9b385db7fb1f05f5a559f190583f324aa75f9d6f30cb1.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 9ced1e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness Symbiotic 1 2018-12-08T18:18 CET (sv-comp)
Download a1b261c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness SMACK 1.9.3 3 2018-12-08T06:10:16
Download 42490fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T23:44:15+01:00 Download 9ced1e8
Download 97d9725 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T22:10:06+01:00 Download a1b261c
Download 3d19b8a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-07T09:18:04+01:00 Download 3f1d88c
Download 41b3f89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T10:10:17+01:00 Download 2d8088e
Download 8fbbb9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:49:07+01:00 Download e03891d
Download 52c6744 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:40:53+01:00 Download 0ae78eb
Download e03891d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T01:49:25+01:00
Download f17bcfd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memcleanup) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:06:42+01:00 Download 6b797ed
Download 4b4763e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-07T23:07 CET (sv-comp)
Download e17896e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 3 2018-12-08T07:00:25
Download 77e2261 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 66 2018-12-07T01:05 CET (sv-comp)
Download 2422c36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 7 2018-12-10T18:33:00+01:00
Download 7f44c26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-07T17:00:10+01:00
Download ef6e2bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-10T20:38:24+01:00 Download 2422c36
Download bc47567 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-10T10:48:56+01:00 Download 4fc1c2d
Download 2413c4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:53:11+01:00 Download 2e427b7
Download f938ba5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:37:33+01:00 Download dc0bcf1
Download 429867b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:28:21+01:00 Download 34688c3
Download 2ddcd4b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 80 2018-12-09T18:19:58+01:00 Download 2ce033c
Download b29302a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T23:43:53+01:00 Download 4b4763e
Download 99a20c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T22:07:29+01:00 Download e17896e
Download 0b25554 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T08:05:47+01:00 Download 7f44c26
Download b42bb8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T04:59:49+01:00 Download 0825bec
Download 78dd999 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T04:22:20+01:00 Download 4fc1c2d
Download 5531d56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 92 2018-12-07T17:43:18+01:00 Download 77e2261
Download 818588d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-07T09:29:01+01:00 Download bb7ada3
Download d8bca9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-07T01:06:07+01:00 Download c75e7b2
Download b3946ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T10:10:18+01:00 Download 7186dd0
Download 754aff9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:48:10+01:00 Download 555c8e8
Download a0091e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:41:39+01:00 Download 37b2486
Download 5c1122b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:16:28+01:00 Download 383b978
Download 9c6809c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:10:37+01:00 Download ddd76bf
Download 555c8e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-05T18:24:57+01:00
Download 2403522 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T11:55 CET (sv-comp)
Download 9551b8a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T09:25 CET (sv-comp)

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

Trying to find witnesses for program (ccdb3117b6c3e0771df9b385db7fb1f05f5a559f190583f324aa75f9d6f30cb1, sv-benchmarks/c/list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i).

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

Found 0 witnesses for program sv-benchmarks/c/list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i, ccdb3117b6c3e0771df9b385db7fb1f05f5a559f190583f324aa75f9d6f30cb1
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ccdb3117b6c3e0771df9b385db7fb1f05f5a559f190583f324aa75f9d6f30cb1.json

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