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/ldv-memsafety/StructInitialization1_true-valid-memsafety.c
programSHA b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585
witnessName results-verified/cbmc.2018-12-04_2248.logfiles/sv-comp19_prop-memsafety.StructInitialization1_true-valid-memsafety.c.files/witness.graphml
witnessSHA 022ff26a23669da28deb09a6c046cb8e099820189600e298ef093d160e315118

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-05T09:54 CET (sv-comp)
error-specification-length Key 'specification' longer than 100 characters.
producer CBMC
programfile ../../sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c
programhash 64d26f08f1705388a8bcbde0799622957ce08f36
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/022ff26a23669da28deb09a6c046cb8e099820189600e298ef093d160e315118.graphml
witness-sha256 022ff26a23669da28deb09a6c046cb8e099820189600e298ef093d160e315118
witness-size 3507
witness-type correctness_witness

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

Trying to find witnesses for program (b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585, sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c).

Found 17 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c, b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c64d642 Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2023-12-18T09:55:44+01:00
Download d20aa26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2023-11-29T20:39:06Z
Download 38c2ebf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-11-30T05:38:34+01:00
Download 99ddafb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 3 2023-12-03T21:47:01+01:00
Download da966d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 3 2023-12-18T01:33:52+01:00
Download 787ce7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-05T10:08:25Z
Download c7ae47c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-04T05:23:26Z
Download e5a7e40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-01T21:00:56Z
Download 12d7108 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 7.4.0 incr 3 2023-12-01T15:42:48Z
Download 4bb3be7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2023-12-18T18:13:26+01:00
Download af9211d 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 121 2023-12-02T15:27:54Z
Download 3b7744b 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:24:18Z
Download 709020e 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 121 2023-12-02T20:54:54Z
Download 097a2d1 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) 4 2023-11-30T22:42:46Z
Download f2a1a17 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 14 2023-12-17T19:43:21+01:00
Download 5abbeef 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 121 2023-11-29T05:49:43Z
Download 04c0b02 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 2LS 5 2023-11-30T23:02:26+01:00

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

Trying to find witnesses for program (b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585, sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c).

Found 13 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c, b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3ca4f1b Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2022-12-09T05:20:24+01:00
Download 9494514 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2022-12-10T14:58:23+01:00
Download 3473209 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 3 2022-12-12T02:09:44+01:00
Download b05b677 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2022-12-10T00:00:14+01:00
Download a0aea5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 3 2022-12-09T02:40:05+01:00
Download 8e826ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2022-12-08T21:47:04Z
Download 04636d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 7.0.0 incr 3 2022-12-18T19:07:59Z
Download cdc8900 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 6.8.0 incr 3 2022-12-25T10:57:23Z
Download b5d6c71 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 121 2022-12-14T08:40:35Z
Download 4b7e4c7 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 121 2022-12-14T22:54:04Z
Download 3d0a7a5 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 14 2022-12-08T03:25:19+01:00
Download 4c7d379 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 121 2022-12-13T12:40:36Z
Download 30679d7 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 2LS 5 2022-12-08T01:19:56+01:00

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

Trying to find witnesses for program (b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585, sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c).

Found 11 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c, b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3fb41db Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2021-12-07T09:28:21+01:00
Download bc66a83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-05T17:55:47+01:00
Download 4188bf6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 3 2021-12-08T20:12:04+01:00
Download b433888 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 3 2021-12-07T02:22:02+01:00
Download 49b8172 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 6.8.0 incr 3 2021-12-08T11:00:39Z
Download a496a99 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 121 2021-12-10T02:24:00Z
Download 111a419 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 121 2021-12-10T08:22:01Z
Download 91c19b2 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 6 2021-12-06T02:22:13+01:00
Download fb5ff3f 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 121 2021-12-06T18:12:06Z
Download e03d2ef 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 2LS 5 2021-12-05T19:36:14+01:00
Download 3a66b25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2021-12-09T09:56:20+01:00

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

Trying to find witnesses for program (b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585, sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c).

Found 3 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c, b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download de8bf11 Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2020-12-06T18:16:43+01:00
Download a7cc415 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2020-12-08T05:11:26+01:00
Download 021c654 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0 3 2020-12-05T14:50:44+01:00

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

Trying to find witnesses for program (b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585, sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c).

Found 2 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c, b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download cff3059 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 3 2019-11-30T12:50:25+01:00
Download 653bcde Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 3 2019-12-01T05:55:52+01:00

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

Trying to find witnesses for program (b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585, sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c).

Found 3 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c, b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 55151d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2018-12-08T00:40 CET (sv-comp)
Download eec067c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 3 2018-12-07T05:44:58+01:00
Download d362f4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-05T18:03:36+01:00

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

Trying to find witnesses for program (b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585, sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c).

Found 8 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c, b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 56fd1cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2017-12-03T00:29 CET (sv-comp)
Download 6594f07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.6.1-svn 5 2017-12-01T09:23:23+01:00
Download b9bfe1b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.6.1-svn 26773 3 2017-12-01T08:25:58+01:00
Download 5cd3f2b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T11:56:29.584798
Download 3ebba9e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T23:23:42.158760
Download 55e3ff1 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 Map2Check 2 2017-12-01T23:54 CET (sv-comp)
Download 321d06f 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 2017-12-01T08:30 CET (sv-comp)
Download 26e87ec 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 2LS 5 2017-12-01T08:20 CET (sv-comp)

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

Trying to find witnesses for program (b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585, sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/StructInitialization1_true-valid-memsafety.c, b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/b5a281f9631a62a08c6928334ef6ea60eabb7bbadcb2bd7487e60124ebe01585.json

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