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/ArraysOfVariableLength2_false-valid-deref-write.c
programSHA db4b4fb03b1dcc2b831885b6cb4b7f01d511832c58de7e20715e49b64db06c6b
witnessName results-verified/esbmc-kind.2018-12-06_1103.logfiles/sv-comp19_prop-memsafety.ArraysOfVariableLength2_false-valid-deref-write.c.files/witness.graphml
witnessSHA 320f53b63e9a62261eec120150c8293499c0a6eb2be596cb76733c3c6408c3c0

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T20:26:26.563690
producer ESBMC 6.0.0 kind
programfile ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-write.c
programhash a6853fb9e064ccfef5e54a8bac94eb86beeed80f
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) )
witness-file witnessFileByHash/320f53b63e9a62261eec120150c8293499c0a6eb2be596cb76733c3c6408c3c0.graphml
witness-sha256 320f53b63e9a62261eec120150c8293499c0a6eb2be596cb76733c3c6408c3c0
witness-size 3626
witness-type violation_witness

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 84dbbc7 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T09:37:16+01:00
Download b8d9812 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2023-11-29T23:11:36Z
Download 0bd171c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 6 2023-12-19T05:28:01+01:00 Download 7ab50bd
Download 8013ffd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 6 2023-12-18T12:03:57+01:00 Download 84dbbc7
Download 8f94e08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 6 2023-12-18T03:08:54+01:00 Download b49782e
Download 58c4505 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 6 2023-12-17T22:11:04+01:00 Download b3a1ebc
Download 21d54a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 6 2023-12-05T14:37:53+01:00 Download f13364c
Download e62d4d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 6 2023-12-04T16:46:24+01:00 Download 47d669c
Download 19da8c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 6 2023-12-04T12:11:51+01:00 Download 8dca703
Download 6083e72 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 6 2023-12-04T02:25:37+01:00 Download c23233a
Download 392b03e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 6 2023-12-03T06:18:36+01:00 Download 262495f
Download 73ca13e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 6 2023-12-01T22:56:05+01:00 Download 78e38dc
Download 39375b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 6 2023-12-01T18:29:59+01:00 Download 0f0b83e
Download 6d24507 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 6 2023-11-30T13:45:25+01:00 Download 2432e46
Download b65a69d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 6 2023-11-30T09:44:12+01:00 Download 8e1a5c3
Download 2432e46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 5 2023-11-30T07:47:27+01:00
Download 26b8469 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 6 2023-11-30T03:02:30+01:00 Download b8d9812
Download 66b5519 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 6 2023-11-29T08:32:02+01:00 Download 6bebd51
Download 1606eb5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 6 2023-11-28T23:49:48+01:00 Download 8e9a1a6
Download c23233a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 6 2023-12-03T23:21:01+01:00
Download b49782e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 7 2023-12-18T01:36:23+01:00
Download 0f0b83e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.4.0 incr 4 2023-12-01T12:16:39Z
Download 8dca703 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 5 2023-12-02T15:42:43Z
Download 262495f 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 5 2023-12-03T03:50:25Z
Download b3a1ebc 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-17T09:16:36+01:00
Download 6bebd51 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 5 2023-11-29T01:04:12Z
Download 8e9a1a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness sv-sanitizers 0.1.1 3 2023-11-28T22:22:28Z
Download 8e1a5c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2023-11-30T08:26:12Z
Download 7ab50bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2023-12-18T20:57:19+01:00
Download f13364c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-05T10:49:25Z
Download 47d669c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-04T13:01:47Z
Download 78e38dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-01T20:40:08Z
Download 8af7891 Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow location: column: 6 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_43f069d3-414a-4f86-85e6-95fa52f7df73/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_-write.c line: 23 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T23:11:36Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_43f069d3-414a-4f86-85e6-95fa52f7df73/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_-write.c : db4b4fb03b1dcc2b831885b6cb4b7f01d511832c58de7e20715e49b64db06c6b input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_43f069d3-414a-4f86-85e6-95fa52f7df73/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_-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 7 2023-11-30T02:59:14+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8f2e05e Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T06:47:58+01:00
Download a9c32a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-12T17:56:53Z
Download 6e58a8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 6 2023-01-29T10:43:55+01:00 Download 79f77d9
Download bad852e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 6 2023-01-29T06:52:48+01:00 Download 54773da
Download efc9af1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 6 2023-01-29T06:38:20+01:00 Download c9935d3
Download cd7f837 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 6 2023-01-29T05:57:12+01:00 Download a9c32a4
Download ec5b8d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 6 2023-01-29T04:19:26+01:00 Download 82f4c3c
Download 59d3fa4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 6 2023-01-29T01:31:20+01:00 Download 2c98ce8
Download 44d929d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 6 2023-01-28T21:05:02+01:00 Download 4b2a503
Download 9e8fc71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 6 2023-01-28T15:43:36+01:00 Download dd733b0
Download d62ae40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 6 2023-01-28T14:20:35+01:00 Download 8f2e05e
Download 0bde932 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 6 2023-01-28T08:57:33+01:00 Download 68d0ea9
Download 8830b55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 6 2023-01-28T06:01:00+01:00 Download d01637e
Download 4325202 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 6 2023-01-28T04:23:27+01:00 Download 904a1e2
Download a7f1238 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 6 2023-01-28T02:20:51+01:00 Download 82dc28e
Download cac0998 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 6 2023-01-28T00:30:31+01:00 Download 2a471d3
Download 68d0ea9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 6 2022-12-10T20:27:09+01:00
Download 2c98ce8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 6 2022-12-11T22:33:50+01:00
Download 4b2a503 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2022-12-09T16:57:28+01:00
Download d01637e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 7 2022-12-09T03:07:09+01:00
Download dd733b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.0.0 incr 4 2022-12-18T16:44:29Z
Download 82dc28e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2022-12-25T10:11:39Z
Download 79f77d9 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 5 2022-12-14T14:59:42Z
Download c9935d3 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 5 2022-12-14T18:50:53Z
Download 904a1e2 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-08T12:15:58+01:00
Download 54773da 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 5 2022-12-13T18:18:26Z
Download 2a471d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2022-12-08T17:02:39Z

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a8d27a4 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T10:06:10+01:00
Download 4eea6eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2021-12-10T17:53:51
Download 80562b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2021-12-07T12:57:32Z
Download f84093c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 6 2021-12-10T21:26:18+01:00 Download c5a67d4
Download 4502d67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 6 2021-12-10T17:27:20+01:00 Download def7b3b
Download a9f6628 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 6 2021-12-10T08:33:49+01:00 Download 275f5a2
Download 27da5c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 6 2021-12-09T15:59:10+01:00 Download 8d291a2
Download beea5f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 6 2021-12-09T06:21:31+01:00 Download 82f4c3c
Download fdbea45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 6 2021-12-08T21:10:21+01:00 Download 38e3033
Download 226ea10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 6 2021-12-08T13:47:17+01:00 Download 56c1d8c
Download 2a9f576 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 6 2021-12-07T19:10:14+01:00 Download 80562b9
Download f7d6eff Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 6 2021-12-07T11:27:54+01:00 Download a8d27a4
Download 67e0340 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 6 2021-12-07T04:55:14+01:00 Download 7420401
Download b440108 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 6 2021-12-07T02:34:40+01:00 Download 2eeb6d9
Download 0ebc2f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 6 2021-12-06T12:47:41+01:00 Download 50d935b
Download c2ec09f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 6 2021-12-06T11:48:50+01:00 Download d6b9c5d
Download 40743f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 6 2021-12-05T20:40:21+01:00 Download aacf0be
Download aacf0be Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 6 2021-12-05T19:14:18+01:00
Download 7420401 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 7 2021-12-07T02:29:53+01:00
Download 56c1d8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2021-12-08T03:44:39Z
Download 275f5a2 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 5 2021-12-10T05:35:23Z
Download def7b3b 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 5 2021-12-10T15:20:14Z
Download d6b9c5d 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 2021-12-06T01:34:18+01:00
Download 2eeb6d9 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 5 2021-12-06T18:36:35Z
Download 50d935b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness SESL 3 2021-12-06T11:51:43+01:00
Download 38e3033 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 6 2021-12-08T18:46:54+01:00
Download 8d291a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 6 2021-12-09T14:16:36+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f83e979 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T18:30:28+01:00
Download 5b8cc52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-11T20:14:16
Download cfbe105 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-08T23:02:02
Download 84e95af Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 6 2020-12-09T21:41:46+01:00 Download cfd993b
Download 01e0d78 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 6 2020-12-09T04:12:17+01:00 Download cfbe105
Download 23b2c8a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 6 2020-12-09T02:05:40+01:00 Download 6287c09
Download f74b670 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 6 2020-12-08T06:36:16+01:00 Download d7ad740
Download 1de60c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 6 2020-12-07T16:38:39+01:00 Download 4276254
Download f8655e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 6 2020-12-06T18:28:51+01:00 Download 22f0d26
Download 4dfdc74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 6 2020-12-05T16:26:07+01:00
Download 32e3dd2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 6 2020-12-06T19:03:49+01:00 Download f83e979
Download 3a422cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 6 2020-12-12T01:29:37+01:00 Download 5b8cc52
Download f5b13c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 6 2020-12-09T22:09:19+01:00 Download 8bdefc1
Download 0861cd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 6 2020-12-06T18:02:28+01:00 Download 4dfdc74
Download 0045e3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 6 2020-12-06T07:50:56+01:00 Download 22f0d26
Download a915126 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 6 2020-12-05T18:30:33+01:00 Download 4dfdc74
Download d7ad740 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 6 2020-12-08T00:01:55+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c61431e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2019-12-01 05:19:37
Download 6d38e72 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 6 2019-12-11T21:39:12+01:00 Download 0fb72a4
Download ebfb423 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 6 2019-12-11T20:54:30+01:00 Download a6f4bf2
Download d80fdb9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 6 2019-12-06T02:41:19+01:00 Download 99697a4
Download acb8d5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 6 2019-12-03T08:01:44+01:00 Download 4400582
Download 4400582 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 6 2019-11-29T19:29:22+01:00
Download 0fb72a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 6 2019-12-01T17:33:04+01:00
Download 7321868 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 6 2019-12-08T00:26:36+01:00 Download 0cdbd58
Download 46611c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 6 2019-12-08T00:06:55+01:00 Download 82f4c3c
Download c5921ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 6 2019-12-07T21:16:14+01:00 Download 08eb08a
Download 62a35ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 6 2019-12-03T08:57:06+01:00 Download 93f9e79
Download d183dcf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 6 2019-12-11T21:57:25+01:00 Download 03564e7
Download e60b6e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 6 2019-12-11T21:09:24+01:00 Download c61431e
Download f27e510 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 6 2019-12-05T20:21:25+01:00 Download b7ec2a6

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ab3c5ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-07T22:59 CET (sv-comp)
Download df49859 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-07T16:51:41+01:00
Download 658e0f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:36:51+01:00 Download 4b40887
Download 7b6ae98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T23:43:38+01:00 Download ab3c5ae
Download b223800 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T08:06:08+01:00 Download df49859
Download 4717cd8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T05:02:14+01:00 Download 320f53b
Download 8145887 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T04:22:45+01:00 Download 3b80735
Download ae93108 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T10:17:09+01:00 Download 838f44d
Download f9d1cde Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:16:52+01:00 Download 4aa9bba
Download f126417 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-07T09:22:32+01:00 Download 5d913c0
Download 48843e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:49:10+01:00 Download 3a1a78f
Download e47891b 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-08T09:10:30
Download 2abe411 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-10T10:48:55+01:00 Download 3b80735
Download 44816b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:53:25+01:00 Download 7a29b28
Download b346cfc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:32:10+01:00 Download c93598a
Download 4ad659b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T22:10:22+01:00 Download e47891b
Download e79bac1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-07T01:20:21+01:00 Download 1fb9cb4
Download a94f830 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:10:32+01:00 Download 73111b6
Download 3a1a78f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T01:14:31+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 62aead1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-02T23:19 CET (sv-comp)
Download 90e3263 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T08:26:23+01:00
Download 15cacf0 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:45:06.627800
Download e86bf4b 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:52:26.893494
Download 9f94f5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 3.1 5 2017-12-01T09:09 CET (sv-comp)
Download 3c0c2fe 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 5 2017-12-03T06:53Z
Download 17a763b 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 5 2017-12-03T03:41Z
Download 16b8e3f 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 2017-12-01T08:19 CET (sv-comp)
Download 7bacf2c 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 5 2017-12-03T04:01Z
Download 5d913c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2017-12-01T21:51 CET (sv-comp)
Download 9fbedfe Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Map2Check 3 2017-12-01T23:49 CET (sv-comp)

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

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

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

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