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/memset_false-valid-deref-write.c
programSHA ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166
witnessName results-verified/uautomizer.2017-12-03_0439.logfiles/sv-comp18.memset_false-valid-deref-write.c.files/witness.graphml
witnessSHA b90cfd95190154c586400bef95d139f53b2266cec71c982567a67ed4eed96fbc

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-03T03:50Z
error-specification-length Key 'specification' longer than 100 characters.
producer Automizer
program-sha256 ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166
programfile /tmp/vcloud-vcloud-master/worker/working_dir_ebca7889-781b-4e03-a983-78577a63ec8e/sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c
programhash 220c5b7d1335976595fe0a31f6bacc2d390016c7
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/b90cfd95190154c586400bef95d139f53b2266cec71c982567a67ed4eed96fbc.graphml
witness-sha256 b90cfd95190154c586400bef95d139f53b2266cec71c982567a67ed4eed96fbc
witness-size 3430
witness-type violation_witness

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

Trying to find witnesses for program (ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166, sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c).

Found 37 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c, ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0165793 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T08:59:30+01:00
Download 40d27f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2023-12-17T00:54:04Z
Download fc792ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2023-11-30T00:08:20Z
Download 9cc845c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-19T15:32:35+01:00 Download 556460f
Download df0523d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-19T05:25:50+01:00 Download 1e4e7e1
Download e2c77cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-18T12:01:20+01:00 Download 0165793
Download 98358a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-18T03:09:24+01:00 Download eac2a19
Download 5930c31 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-17T22:10:13+01:00 Download d4c1e49
Download e93d281 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-17T06:37:59+01:00 Download 40d27f7
Download bf70006 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-05T14:36:48+01:00 Download 485aaaa
Download f8cf720 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-04T16:45:27+01:00 Download 5ca3552
Download ebcf0a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-04T02:26:17+01:00 Download c484d2e
Download 6403ce5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-01T22:53:57+01:00 Download 462c7a8
Download f0ac41c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T13:44:40+01:00 Download e5c24ea
Download 6a9ae0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T09:44:24+01:00 Download 3a5ce97
Download e5c24ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T09:11:49+01:00
Download 33a65d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T03:03:42+01:00 Download fc792ba
Download 56bebdb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-28T23:49:32+01:00 Download 1038373
Download c484d2e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 3 2023-12-03T21:22:32+01:00
Download 1e4e7e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2023-12-19T00:28:11+01:00
Download eac2a19 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 3 2023-12-18T02:15:51+01:00
Download 18c5038 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-12-04T12:12:10+01:00 Download 4c02b4b
Download b575348 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-12-03T06:19:04+01:00 Download 6273e06
Download 91eb3ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-12-01T18:27:11+01:00 Download 3133eca
Download b7b219d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-11-29T08:33:16+01:00 Download c19431e
Download 3133eca Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.4.0 incr 4 2023-12-01T14:47:34Z
Download 556460f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 3 2023-12-19T10:55:25+01:00
Download 4c02b4b 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 Taipan 4 2023-12-02T17:12:53Z
Download 6273e06 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 Kojak 4 2023-12-02T23:31:52Z
Download d4c1e49 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 3 2023-12-17T08:53:56+01:00
Download c19431e 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 Automizer 4 2023-11-28T23:16:14Z
Download 1038373 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness sv-sanitizers 0.1.1 3 2023-11-28T21:35:33Z
Download 3a5ce97 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2023-11-30T08:24:58Z
Download 485aaaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-05T10:04:27Z
Download 5ca3552 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-04T09:44:58Z
Download 462c7a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-01T21:05:59Z
Download 03ae9e2 Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow location: column: 3 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_cb352223-50cb-425b-a1e9-0b3302338f96/sv-benchmarks/c/ldv-memsafety/memset_-write.c line: 27 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-30T00:08:20Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_cb352223-50cb-425b-a1e9-0b3302338f96/sv-benchmarks/c/ldv-memsafety/memset_-write.c : ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_cb352223-50cb-425b-a1e9-0b3302338f96/sv-benchmarks/c/ldv-memsafety/memset_-write.c language: C specification: CHECK( init(main()), LTL(G valid-free) ),CHECK( init(main()), LTL(G valid-deref) ),CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 4 2023-11-30T03:00:23+01:00

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

Trying to find witnesses for program (ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166, sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c).

Found 29 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c, ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e8d59a1 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T05:15:04+01:00
Download 57cc314 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-25T10:03:30Z
Download 8df8251 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-12T11:53:03Z
Download f455bd7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T05:58:13+01:00 Download 8df8251
Download 4683749 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T04:19:23+01:00 Download afea95f
Download 992c265 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T01:31:07+01:00 Download a01adb8
Download 8d390dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T00:53:41+01:00 Download 9042a06
Download d26590a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T21:07:44+01:00 Download bbb4a94
Download cbd769a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T14:12:00+01:00 Download e8d59a1
Download 088e7f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T08:54:58+01:00 Download e54273e
Download 24a8cf0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T06:01:23+01:00 Download 84d511f
Download 4b3422b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T04:21:50+01:00 Download 1dedbfd
Download f50791b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T02:23:37+01:00 Download 57cc314
Download db4155a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T00:28:24+01:00 Download 7c78617
Download e54273e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2022-12-10T21:43:34+01:00
Download a01adb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 3 2022-12-11T22:08:32+01:00
Download 9042a06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2022-12-11T04:17:37+01:00
Download 84d511f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 3 2022-12-09T02:39:41+01:00
Download d64fb14 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-29T10:45:27+01:00 Download c128622
Download 478881b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-29T06:53:12+01:00 Download 4997e74
Download 52c07d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-29T06:39:08+01:00 Download 97b33bb
Download e07c982 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-28T15:45:00+01:00 Download 630b291
Download 630b291 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.0.0 incr 4 2022-12-18T22:16:03Z
Download c128622 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 Taipan 4 2022-12-14T11:32:51Z
Download 97b33bb 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 Kojak 4 2022-12-15T02:51:12Z
Download 1dedbfd 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 3 2022-12-08T11:05:23+01:00
Download 4997e74 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 Automizer 4 2022-12-13T18:44:50Z
Download bbb4a94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2022-12-10T04:06:37+01:00
Download 7c78617 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2022-12-08T16:58:18Z

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

Trying to find witnesses for program (ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166, sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c).

Found 25 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c, ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 9eae3b3 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T07:54:01+01:00
Download b536537 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2021-12-10T17:31:30
Download 5fa6270 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2021-12-07T14:50:15Z
Download cb7b91d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-10T21:29:22+01:00 Download b536537
Download ab61a9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-09T16:02:26+01:00 Download 2d76bb8
Download f36813c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-09T06:21:29+01:00 Download afea95f
Download 0113b3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-08T21:08:15+01:00 Download 03e8e3a
Download d47151c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T19:10:16+01:00 Download 5fa6270
Download 32090b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T11:27:59+01:00 Download 9eae3b3
Download c2fe693 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T04:56:05+01:00 Download 615b718
Download 9f100fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-06T11:49:36+01:00 Download 7dfa5ce
Download f3a6ae0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-05T20:38:37+01:00 Download bee1457
Download bee1457 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-05T15:02:35+01:00
Download 615b718 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 3 2021-12-07T03:56:36+01:00
Download 84df84b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-10T17:27:12+01:00 Download 2111fe7
Download 3cea1ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-10T08:34:05+01:00 Download a7f2562
Download e6fde00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-08T13:49:08+01:00 Download ddfc50a
Download 0bdeca8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-07T02:35:10+01:00 Download f92a6b4
Download ddfc50a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2021-12-08T04:22:48Z
Download a7f2562 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 Taipan 4 2021-12-10T04:14:48Z
Download 2111fe7 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 Kojak 4 2021-12-10T07:09:09Z
Download 7dfa5ce 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 3 2021-12-05T14:26:29+01:00
Download f92a6b4 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 Automizer 4 2021-12-06T17:22:48Z
Download 03e8e3a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 3 2021-12-08T19:53:34+01:00
Download 2d76bb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2021-12-09T13:52:41+01:00

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

Trying to find witnesses for program (ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166, sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c).

Found 17 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c, ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0a5f011 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T18:45:17+01:00
Download 6db179f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-11T19:03:30
Download aa7855a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-09T02:09:08
Download c631dc1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-09T04:12:27+01:00 Download aa7855a
Download 47ccb99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-09T02:29:21+01:00 Download d5c66a6
Download f0a592f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-06T18:02:07+01:00 Download 3e95adf
Download 6b2da2a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-06T07:49:42+01:00 Download b0a3926
Download 0388ac5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-05T18:04:18+01:00 Download 3e95adf
Download 3e95adf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-05T15:41:36+01:00
Download 1951ab3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 3 2020-12-09T21:52:49+01:00 Download fe2c331
Download fb97f24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 3 2020-12-06T18:25:50+01:00 Download b0a3926
Download ea83a00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2020-12-08T05:35:07+01:00
Download 0580224 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0 3 2020-12-07T16:38:57+01:00 Download 5c15e3e
Download dea6fcf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-12T01:45:11+01:00 Download 6db179f
Download b92ae26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-09T22:12:39+01:00 Download 28b1541
Download 536fa66 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-08T07:55:04+01:00 Download ea83a00
Download d36ef7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-06T19:10:34+01:00 Download 0a5f011

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

Trying to find witnesses for program (ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166, sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c).

Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c, ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ac90aa6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2019-12-01 03:20:20
Download f2a5dfe Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-11T22:00:45+01:00 Download b85b6a6
Download a3e17b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:43:43+01:00 Download ba33c3e
Download 8f9e321 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:09:42+01:00 Download ac90aa6
Download 968dce1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-08T00:27:09+01:00 Download b40073e
Download 70d7078 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-06T02:38:42+01:00 Download f7b2a25
Download 273a605 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-05T20:20:47+01:00 Download f880d86
Download 58bb5e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-03T08:57:52+01:00 Download acd47f7
Download 45b92b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 3 2019-12-11T20:54:26+01:00 Download 6b462e5
Download 0c6f5c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 3 2019-12-07T21:16:06+01:00 Download 3653244
Download 6637c16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 3 2019-11-30T00:18:46+01:00
Download b85b6a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 3 2019-12-01T10:49:17+01:00
Download 17944f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 3 2019-12-08T00:06:01+01:00 Download afea95f
Download a1c99b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 3 2019-12-03T08:09:32+01:00 Download 6637c16

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

Trying to find witnesses for program (ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166, sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c).

Found 18 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c, ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b0e3cf6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T10:05 CET (sv-comp)
Download 93438cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 3 2018-12-07T01:40:02+01:00
Download c67087d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-10T10:48:55+01:00 Download 40154ac
Download 7682c7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:39:18+01:00 Download 9eb8c59
Download fc83a47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T23:41:56+01:00 Download b0e3cf6
Download 309aa65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T22:07:24+01:00 Download b18931b
Download f917db8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T08:00:30+01:00 Download 93438cb
Download f52b0b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T04:17:06+01:00 Download 40154ac
Download 58f79d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:48:44+01:00 Download d92985d
Download b59efbb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:09:43+01:00 Download 4f97927
Download d92985d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T05:15:27+01:00
Download 4bbe5c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-06T10:18:14+01:00 Download fa40e22
Download c449ecd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-07T09:30:15+01:00 Download 1dd8a11
Download b18931b 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-08T02:00:33
Download 6a176bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:53:17+01:00 Download afb68eb
Download 6c6a8a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:26:42+01:00 Download 5f0b1e2
Download 54a1675 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:19:30+01:00 Download f3f5b09
Download ceab00f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-08T05:03:08+01:00 Download d15d4ea

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

Trying to find witnesses for program (ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166, sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c).

Found 11 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c, ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 90c067c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-03T00:25 CET (sv-comp)
Download 6a7f6dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.6.1-svn 26773 3 2017-12-01T08:23:23+01:00
Download 6dfb4c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T10:52:24.859348
Download 1797bab Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T23:47:32.945975
Download 0d6cfcd 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 Taipan 3 2017-12-03T06:53Z
Download bd38d0f 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 Kojak 4 2017-12-03T04:18Z
Download db555a2 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 Forester 4 2017-12-01T19:28 CET (sv-comp)
Download 42c735f 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 4 2017-12-01T08:24 CET (sv-comp)
Download b90cfd9 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 Automizer 3 2017-12-03T03:50Z
Download 1dd8a11 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2017-12-01T22:02 CET (sv-comp)
Download 35459bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Map2Check 2 2017-12-01T23:42 CET (sv-comp)

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

Trying to find witnesses for program (ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166, sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c).

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

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