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-ext3/scopes4_true-valid-memsafety.c
programSHA 58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606
witnessName results-verified/utaipan.2018-12-08_1419.logfiles/sv-comp19_prop-memsafety.scopes4_true-valid-memsafety.c.files/witness.graphml
witnessSHA f7ae297a4249a8e03ab40d059a5a1a8b370a9b68c6a5b83f29192a7fa781b783

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-09T18:36Z
error-specification-length Key 'specification' longer than 100 characters.
producer Taipan
programfile /tmp/vcloud-vcloud-master/worker/working_dir_fa4ebb92-bc92-4998-8c96-d075c236542e/sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c
programhash 87dcbb1d4539995e5aba39e6053775ca0fac811e
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )
witness-file witnessFileByHash/f7ae297a4249a8e03ab40d059a5a1a8b370a9b68c6a5b83f29192a7fa781b783.graphml
witness-sha256 f7ae297a4249a8e03ab40d059a5a1a8b370a9b68c6a5b83f29192a7fa781b783
witness-size 6073
witness-type correctness_witness

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

Trying to find witnesses for program (58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606, sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c).

Found 15 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c, 58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 999f3eb Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2023-12-18T10:32:58+01:00
Download 1d304ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2023-11-29T23:10:48Z
Download d313c5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 4 2023-11-30T04:50:51+01:00
Download 153e4ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 4 2023-12-03T23:10:58+01:00
Download df6a0f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 5 2023-12-18T01:35:57+01:00
Download f17b780 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-05T11:33:31Z
Download 2320970 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-04T14:28:57Z
Download 188b2f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-01T20:26:09Z
Download 9a59bac Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 7.4.0 incr 3 2023-12-01T14:10:34Z
Download f0fb379 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 7 2023-12-02T11:22:11Z
Download b61fefd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness PredatorHP 4 2023-11-30T08:25:30Z
Download 7832657 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T08:47:19Z
Download f91c178 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 6 2023-12-01T01:14:52Z
Download 472dee6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CBMC 4 2023-12-17T11:20:28+01:00
Download b3e5b24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2023-12-18T18:44:48+01:00

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

Trying to find witnesses for program (58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606, sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c).

Found 11 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c, 58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d59c91c Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2022-12-09T06:47:41+01:00
Download 0e45839 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 4 2022-12-10T14:48:01+01:00
Download f1957fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 4 2022-12-12T01:44:43+01:00
Download 9a14a5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 5 2022-12-09T02:57:45+01:00
Download 98aba79 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2022-12-08T20:46:34Z
Download 461e0d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 7.0.0 incr 3 2022-12-18T20:12:28Z
Download ee4e3c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 6.8.0 incr 3 2022-12-25T08:29:41Z
Download ec57e02 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 7 2022-12-14T06:26:37Z
Download fcaa524 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T10:55:59Z
Download a87bdf4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CBMC 4 2022-12-08T05:30:52+01:00
Download e99be05 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2022-12-10T01:41:46+01:00

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

Trying to find witnesses for program (58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606, sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c).

Found 11 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c, 58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3b867ad Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2021-12-07T09:17:53+01:00
Download 9097bde Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 4 2021-12-05T18:52:29+01:00
Download a1ba210 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 4 2021-12-09T10:31:28+01:00
Download d6b04b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 5 2021-12-07T01:55:33+01:00
Download bd52bdd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 6.8.0 incr 3 2021-12-08T05:32:15Z
Download da711e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 4 2021-12-08T18:18:18+01:00
Download c668db2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 7 2021-12-10T05:52:34Z
Download a25d753 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Kojak 7 2021-12-10T09:03:59Z
Download 3a9db48 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CBMC 4 2021-12-06T07:40:38+01:00
Download 66887f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 7 2021-12-06T19:58:51Z
Download de4bce5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness SESL 2 2021-12-06T11:30:53+01:00

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

Trying to find witnesses for program (58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606, sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c).

Found 3 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c, 58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6a2d4c3 Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2020-12-06T17:40:48+01:00
Download 20d5d21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 4 2020-12-05T16:54:01+01:00
Download a955d8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 4 2020-12-07T22:29:11+01:00

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

Trying to find witnesses for program (58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606, sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c).

Found 2 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c, 58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ab78acb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 4 2019-11-29T21:26:55+01:00
Download b14861d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 4 2019-12-01T17:58:15+01:00

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

Trying to find witnesses for program (58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606, sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c).

Found 3 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c, 58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 48c7281 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2018-12-08T08:03 CET (sv-comp)
Download 69bccf4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-07T10:42:29+01:00
Download fe0c781 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-05T14:47:08+01:00

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

Trying to find witnesses for program (58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606, sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c).

Found 0 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c, 58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606.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 (58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606, sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c).

Found 0 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes4_true-valid-memsafety.c, 58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/58596999bba5cc256a412be61e4f9e3e6d264c81e8972a76406a7a850d8c4606.json

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