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).

This link does not point to a witness, but below is a list of witnesses for the same program.

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

Trying to find witnesses for program (07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740, sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c).

Found 33 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c, 07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e4ee27b Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T09:47:22+01:00
Download 7da2839 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2023-11-29T20:49:14Z
Download 74e0977 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 7 2023-12-19T05:27:03+01:00 Download aa0040a
Download 4e538b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 7 2023-12-18T12:07:26+01:00 Download e4ee27b
Download 08cfc6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 7 2023-12-18T03:09:38+01:00 Download a212266
Download 3eda256 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 7 2023-12-17T22:11:13+01:00 Download 870bb62
Download 07640ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 7 2023-12-05T14:38:51+01:00 Download 8410a12
Download 69c2af8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 7 2023-12-04T16:44:21+01:00 Download 73758f5
Download 5c51337 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 7 2023-12-04T12:13:32+01:00 Download b884404
Download b446a2f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 7 2023-12-04T02:27:19+01:00 Download 57bcf15
Download 17f49b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 7 2023-12-03T06:18:09+01:00 Download 849a20b
Download 2069006 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 7 2023-12-01T22:55:20+01:00 Download 5f9a881
Download 395e7a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 7 2023-12-01T18:29:22+01:00 Download 55fc0dc
Download b5ba090 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 7 2023-11-30T13:42:36+01:00 Download 52f8297
Download 691820a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 7 2023-11-30T09:44:00+01:00 Download e9171ea
Download 52f8297 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 6 2023-11-30T06:36:53+01:00
Download 53fc346 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 7 2023-11-30T03:02:16+01:00 Download 7da2839
Download 35aa49d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 7 2023-11-29T08:33:03+01:00 Download e8bd7c0
Download b0301ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 7 2023-11-28T23:49:35+01:00 Download 15a17c3
Download 57bcf15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 7 2023-12-03T18:10:55+01:00
Download a212266 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 9 2023-12-18T01:45:53+01:00
Download 55fc0dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.4.0 incr 4 2023-12-01T11:40:05Z
Download b884404 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 6 2023-12-02T16:00:34Z
Download 849a20b 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 6 2023-12-03T00:16:29Z
Download 870bb62 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 2023-12-17T18:55:53+01:00
Download e8bd7c0 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 6 2023-11-28T19:21:46Z
Download 15a17c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness sv-sanitizers 0.1.1 3 2023-11-28T22:16:00Z
Download e9171ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2023-11-30T08:24:59Z
Download aa0040a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 7 2023-12-18T20:34:05+01:00
Download 8410a12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-05T07:54:05Z
Download 73758f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-04T13:43:18Z
Download 5f9a881 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-01T20:29:21Z
Download ac9590a Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow location: column: 6 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3805094c-8c90-449b-b5b9-04856a8043a3/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_-read.c line: 14 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T20:49:14Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3805094c-8c90-449b-b5b9-04856a8043a3/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_-read.c : 07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3805094c-8c90-449b-b5b9-04856a8043a3/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_-read.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 8 2023-11-30T02:58:20+01:00

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

Trying to find witnesses for program (07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740, sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c).

Found 27 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c, 07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7c102d0 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T05:21:12+01:00
Download 2080a64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-12T14:27:30Z
Download a721342 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 7 2023-01-29T10:45:05+01:00 Download a586923
Download 9b92e7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 7 2023-01-29T06:52:34+01:00 Download d4109ff
Download 47a236b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 7 2023-01-29T06:38:37+01:00 Download 62dce7e
Download bdb243b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 7 2023-01-29T05:57:57+01:00 Download 2080a64
Download be763e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 7 2023-01-29T04:19:26+01:00 Download ac1ea66
Download e3c9b6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 7 2023-01-29T01:30:26+01:00 Download dd80107
Download 1da958f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 7 2023-01-28T21:05:52+01:00 Download 1553d6b
Download 0150b36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 7 2023-01-28T15:43:20+01:00 Download a5bc219
Download 641eea8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 7 2023-01-28T14:18:10+01:00 Download 7c102d0
Download 63070c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 7 2023-01-28T08:54:41+01:00 Download 038e428
Download d7493d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 7 2023-01-28T06:01:11+01:00 Download 55f6792
Download d4551b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 7 2023-01-28T04:22:31+01:00 Download 3419557
Download 6696efe Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 7 2023-01-28T02:21:10+01:00 Download bf8d990
Download 42a85c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 7 2023-01-28T00:29:22+01:00 Download a56ce22
Download 038e428 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 7 2022-12-10T15:18:24+01:00
Download dd80107 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 7 2022-12-11T21:41:05+01:00
Download 55f6792 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 9 2022-12-09T03:00:31+01:00
Download a5bc219 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.0.0 incr 4 2022-12-18T17:33:39Z
Download bf8d990 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2022-12-25T09:54:33Z
Download a586923 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 6 2022-12-14T12:39:42Z
Download 62dce7e 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 6 2022-12-14T20:57:20Z
Download 3419557 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 2022-12-08T04:23:21+01:00
Download d4109ff 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 6 2022-12-13T18:15:17Z
Download 1553d6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 7 2022-12-10T01:52:21+01:00
Download a56ce22 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2022-12-08T20:56:07Z

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

Trying to find witnesses for program (07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740, sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c).

Found 27 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c, 07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ee728da Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T09:28:25+01:00
Download 993bcd9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2021-12-10T16:07:40
Download ede0f5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2021-12-07T13:49:27Z
Download f7190b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 7 2021-12-10T21:28:31+01:00 Download 7fce120
Download 99ec8d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 7 2021-12-10T17:27:06+01:00 Download f42ec0a
Download 932a090 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 7 2021-12-10T08:33:04+01:00 Download 990da96
Download 6c60cb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 7 2021-12-09T16:02:48+01:00 Download a9f942f
Download 829951c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 7 2021-12-09T06:21:45+01:00 Download ac1ea66
Download 50525d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 7 2021-12-08T21:06:55+01:00 Download 5eeee43
Download 6ab65b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 7 2021-12-08T13:50:11+01:00 Download 7c133d8
Download 63ce947 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 7 2021-12-07T19:13:43+01:00 Download ede0f5f
Download a1c418f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 7 2021-12-07T11:27:54+01:00 Download ee728da
Download 6c18144 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 7 2021-12-07T04:55:56+01:00 Download 0887c5c
Download 51932b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 7 2021-12-07T02:36:10+01:00 Download 3ebd01e
Download bdfdc7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 7 2021-12-06T12:47:38+01:00 Download 3e93b96
Download cc310ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 7 2021-12-05T20:39:04+01:00 Download 48f7d1c
Download 48f7d1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 7 2021-12-05T15:40:26+01:00
Download 5eeee43 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 7 2021-12-08T18:06:51+01:00
Download a9f942f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 7 2021-12-09T14:10:18+01:00
Download 0887c5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 9 2021-12-07T02:12:05+01:00
Download 5cd6662 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 11 2021-12-06T11:48:21+01:00 Download aef452d
Download 7c133d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2021-12-08T09:42:22Z
Download 990da96 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 6 2021-12-10T04:03:51Z
Download f42ec0a 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 6 2021-12-10T08:44:06Z
Download aef452d 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 5 2021-12-06T02:08:54+01:00
Download 3ebd01e 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 6 2021-12-06T17:19:39Z
Download 3e93b96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness SESL 3 2021-12-06T11:17:09+01:00

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

Trying to find witnesses for program (07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740, sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c).

Found 17 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c, 07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8f19a21 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T17:54:50+01:00
Download 12bfac8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-11T15:25:17
Download 8657117 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-08T19:17:36
Download 21fd983 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 7 2020-12-09T21:55:52+01:00 Download 6eb6a1f
Download 3adfce3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 7 2020-12-07T16:54:17+01:00 Download 1391632
Download 9a44b95 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 7 2020-12-06T19:38:46+01:00 Download 8f19a21
Download b2cb6cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 7 2020-12-08T00:00:40+01:00
Download e708d5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 7 2020-12-09T21:31:15+01:00 Download 3acb7f1
Download 536d45f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 7 2020-12-09T02:02:43+01:00 Download 0395eec
Download 601f5cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 7 2020-12-08T07:27:57+01:00 Download b2cb6cb
Download 8806887 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0 11 2020-12-06T18:25:22+01:00 Download 3c4dc01
Download 959cfa9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0 11 2020-12-06T07:34:54+01:00 Download 3c4dc01
Download 59c340e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 7 2020-12-12T01:36:39+01:00 Download 12bfac8
Download 72c3e55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 7 2020-12-09T03:58:36+01:00 Download 8657117
Download 399131e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 7 2020-12-06T18:00:54+01:00 Download 33c2d11
Download 16ffb8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 7 2020-12-05T18:29:16+01:00 Download 33c2d11
Download 33c2d11 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 7 2020-12-05T16:36:39+01:00

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

Trying to find witnesses for program (07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740, sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c).

Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c, 07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download faf3bd8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2019-12-01 11:49:18
Download 552514e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 7 2019-12-11T21:43:16+01:00 Download 03d3a92
Download f95a16b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 7 2019-12-11T20:54:47+01:00 Download cb4c562
Download d351417 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 7 2019-12-06T02:40:49+01:00 Download 159d902
Download 441f7a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 7 2019-12-03T08:10:10+01:00 Download 2b2b699
Download 2b2b699 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 7 2019-11-30T11:46:20+01:00
Download 21a4fd7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 7 2019-12-01T09:20:16+01:00
Download 46bb0e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 7 2019-12-11T21:09:44+01:00 Download faf3bd8
Download f09675e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 7 2019-12-07T21:16:17+01:00 Download 893da6b
Download ed485bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 10 2019-12-05T20:20:40+01:00 Download 938662c
Download 6e9826d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 7 2019-12-11T21:53:32+01:00 Download 21a4fd7
Download ee54270 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 7 2019-12-08T00:27:17+01:00 Download a63a3c0
Download 351ebf0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 7 2019-12-08T00:06:03+01:00 Download ac1ea66
Download b27fccc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 7 2019-12-03T08:56:49+01:00 Download 0c50a71

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

Trying to find witnesses for program (07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740, sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c).

Found 19 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c, 07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 9276cdd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T02:27 CET (sv-comp)
Download 765acf5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-10T10:48:43+01:00 Download 46df281
Download 24acc24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T23:42:36+01:00 Download 9276cdd
Download 511a348 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T08:56:13+01:00 Download cae3cd2
Download 98526d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:48:01+01:00 Download 0c16d0a
Download 0c16d0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-05T10:18:17+01:00
Download cf0bb5a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-06T09:18:59+01:00 Download 59e1a70
Download d7b49c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-06T09:18:04+01:00 Download 2bd5a0d
Download 5bcf470 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:37:09+01:00 Download e732d9b
Download 1b69117 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-07T09:24:59+01:00 Download 809f85b
Download 2ac396b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T10:19:11+01:00 Download 1cf155e
Download d59001c 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-08T05:49:08
Download cae3cd2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 7 2018-12-06T20:02:40+01:00
Download 3a34468 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:53:23+01:00 Download ffb2edd
Download c3f493c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:21:38+01:00 Download c236f59
Download 52df65c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T22:10:02+01:00 Download d59001c
Download 1229ee2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T05:04:22+01:00 Download 48ea5a0
Download c6812c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T03:36:09+01:00 Download 46df281
Download 405415a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-07T01:16:49+01:00 Download a8ff427

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

Trying to find witnesses for program (07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740, sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c).

Found 11 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c, 07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 97c09aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-03T00:20 CET (sv-comp)
Download d1a8633 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:49:15.844043
Download cb112be 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:14:33.827777
Download 5fdb2d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 3.1 5 2017-12-01T09:38 CET (sv-comp)
Download ab404a3 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 6 2017-12-03T06:58Z
Download fc03110 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 6 2017-12-03T04:12Z
Download ff34165 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 6 2017-12-01T08:31 CET (sv-comp)
Download dd58e91 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 6 2017-12-03T04:06Z
Download 809f85b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2017-12-01T22:03 CET (sv-comp)
Download cbea6ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Map2Check 4 2017-12-01T23:39 CET (sv-comp)
Download 9497faf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T08:31:06+01:00

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

Trying to find witnesses for program (07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740, sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c, 07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740.json

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