Witness Inspection

A description of this web service can be found in the CAV paper "Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses" (more material).

View and Validate the Witness

Input Given to this Service about the Witness (URL Query)

Key Value
programName sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c
programSHA ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6
witnessName results-validated/cpa-seq-validate-violation-witnesses-divine-smt.2018-12-08_0324.logfiles/sv-comp19_prop-memsafety.getNumbers1_false-valid-deref.c.files/witness.graphml
witnessSHA f4559fee1b8a8f853b3f58abfb77da239ac5d49c898c3c253c9f96f8a624304f

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-08T04:33:32+01:00
inputwitnesshash ab28e3bb61b4b98489dbd5f635af54b92127309927bf90b53dfe5f2cb04c986e
producer CPAchecker 1.7-svn 29852
program-sha256 ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6
programfile ../../sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c
programhash ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-deref) )
witness-file witnessFileByHash/f4559fee1b8a8f853b3f58abfb77da239ac5d49c898c3c253c9f96f8a624304f.graphml
witness-sha256 f4559fee1b8a8f853b3f58abfb77da239ac5d49c898c3c253c9f96f8a624304f
witness-size 15187
witness-type violation_witness

This witness was created for this program (cf. table above, ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6).

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

Trying to find witnesses for program (ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6, sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c).

Found 30 witnesses for program sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c, ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0ed4aab Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T10:29:36+01:00
Download bd3c1b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2023-11-29T23:32:05Z
Download ea63cfb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 15 2023-12-19T05:26:46+01:00 Download e811df7
Download b5f0c90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 15 2023-12-18T12:06:56+01:00 Download 0ed4aab
Download b087cf7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 15 2023-12-17T22:10:54+01:00 Download e324efc
Download 1b058a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 15 2023-12-05T14:40:57+01:00 Download fb3f93d
Download 4ef171f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 15 2023-12-04T16:45:13+01:00 Download 826e983
Download 7bbee8a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 15 2023-12-04T12:11:57+01:00 Download 5b5ce81
Download 1e27fce Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 15 2023-12-04T02:25:34+01:00 Download 036d545
Download d6c1efe Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 15 2023-12-03T06:18:23+01:00 Download bb936fa
Download c6ce26b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 15 2023-12-01T22:53:47+01:00 Download 48075f6
Download 7d0d449 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 15 2023-11-30T13:44:23+01:00 Download d6aedea
Download 5d4327c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 15 2023-11-30T09:44:20+01:00 Download 361e8d9
Download d6aedea Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 13 2023-11-30T09:03:42+01:00
Download 09e49e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 15 2023-11-30T03:06:04+01:00 Download bd3c1b8
Download 69dc626 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 15 2023-11-29T08:32:08+01:00 Download 1f27a2f
Download 036d545 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 15 2023-12-04T00:38:29+01:00
Download e811df7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 15 2023-12-18T21:40:09+01:00
Download d0000f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 6 2023-12-01T18:28:44+01:00 Download f3600e0
Download ce0ed9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 7 2023-12-18T01:45:44+01:00
Download f3600e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.4.0 incr 12 2023-12-01T13:51:35Z
Download 5b5ce81 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 13 2023-12-02T15:55:16Z
Download bb936fa 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 13 2023-12-03T01:35:49Z
Download e324efc 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 2023-12-17T12:58:49+01:00
Download 1f27a2f 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 13 2023-11-29T03:12:55Z
Download 361e8d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2023-11-30T08:24:02Z
Download fb3f93d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-05T10:25:09Z
Download 826e983 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-04T13:43:58Z
Download 48075f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-01T21:18:56Z
Download e4fbe78 Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow location: column: 7 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f95cfd60-e0c4-460f-9cbe-e33685b89e0b/sv-benchmarks/c/memsafety-ext3/getNumbers1-1.c line: 11 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T23:32:05Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f95cfd60-e0c4-460f-9cbe-e33685b89e0b/sv-benchmarks/c/memsafety-ext3/getNumbers1-1.c : ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f95cfd60-e0c4-460f-9cbe-e33685b89e0b/sv-benchmarks/c/memsafety-ext3/getNumbers1-1.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 16 2023-11-30T02:58:51+01:00

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

Trying to find witnesses for program (ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6, sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c).

Found 26 witnesses for program sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c, ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5490b7f Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T06:30:56+01:00
Download 492b38e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-12T13:22:23Z
Download 2d232c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 15 2023-01-29T10:44:16+01:00 Download 0f60f5a
Download ba7bad4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 15 2023-01-29T06:53:27+01:00 Download dc45fab
Download 4cd71ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 15 2023-01-29T06:38:01+01:00 Download 0a903d2
Download 714b0b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 15 2023-01-29T05:58:47+01:00 Download 492b38e
Download 228dd09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 15 2023-01-29T04:19:25+01:00 Download c3c2f34
Download 38332c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 15 2023-01-29T01:30:53+01:00 Download c4ea0b4
Download 2e8769f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 15 2023-01-28T21:06:18+01:00 Download 2bce36b
Download 517ef0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 15 2023-01-28T14:09:21+01:00 Download 5490b7f
Download 6e8f5ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 15 2023-01-28T08:56:02+01:00 Download 6500b71
Download 4472fe1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 15 2023-01-28T04:21:52+01:00 Download e5425aa
Download 93ebe4f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 15 2023-01-28T00:28:18+01:00 Download 15ed886
Download 6500b71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 15 2022-12-10T21:28:07+01:00
Download c4ea0b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 15 2022-12-12T00:44:20+01:00
Download 2bce36b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 15 2022-12-10T02:07:50+01:00
Download 868a182 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 7 2023-01-28T15:43:36+01:00 Download 0319f61
Download 644cb69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 7 2023-01-28T02:22:43+01:00 Download 1ce8447
Download 211dc39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 7 2022-12-09T03:12:00+01:00
Download 0319f61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.0.0 incr 12 2022-12-18T21:18:39Z
Download 1ce8447 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 12 2022-12-25T09:28:25Z
Download 0f60f5a 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 13 2022-12-14T04:16:15Z
Download 0a903d2 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 13 2022-12-14T15:35:01Z
Download e5425aa 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 2022-12-08T07:02:14+01:00
Download dc45fab 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 13 2022-12-13T13:08:35Z
Download 15ed886 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2022-12-08T15:48:19Z

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

Trying to find witnesses for program (ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6, sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c).

Found 24 witnesses for program sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c, ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8379b74 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T09:39:59+01:00
Download c97a097 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2021-12-07T14:11:14Z
Download 36b8041 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 15 2021-12-10T21:29:17+01:00 Download 68e17bf
Download 5a565a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 15 2021-12-10T17:27:33+01:00 Download 3c87532
Download 3dad931 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 15 2021-12-10T08:33:37+01:00 Download 44e125c
Download 41e874f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 15 2021-12-09T16:02:04+01:00 Download 8f3bfe5
Download b2759ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 15 2021-12-09T06:21:07+01:00 Download c3c2f34
Download 90a56c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 15 2021-12-08T21:10:47+01:00 Download 27344f2
Download 8a445b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 5 2021-12-07T19:09:54+01:00 Download c97a097
Download 3aaaa82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 15 2021-12-07T11:26:37+01:00 Download 8379b74
Download a4fefb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 15 2021-12-07T02:36:15+01:00 Download b67e373
Download 2a0e0cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 15 2021-12-06T11:46:36+01:00 Download 1c0c863
Download 869f64f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 15 2021-12-05T20:41:30+01:00 Download 722bead
Download 722bead Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 15 2021-12-05T16:16:08+01:00
Download 68e17bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 15 2021-12-10T18:32:09+01:00
Download 27344f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 15 2021-12-08T18:44:19+01:00
Download 8f3bfe5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 15 2021-12-09T14:14:06+01:00
Download 3244b65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 7 2021-12-08T13:45:36+01:00 Download 85bd301
Download 12d23b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 7 2021-12-07T02:41:29+01:00
Download 85bd301 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 12 2021-12-08T04:02:07Z
Download 44e125c 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 13 2021-12-09T23:38:47Z
Download 3c87532 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 13 2021-12-10T13:05:33Z
Download 1c0c863 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 11 2021-12-06T04:28:17+01:00
Download b67e373 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 13 2021-12-06T17:26:23Z

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

Trying to find witnesses for program (ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6, sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c).

Found 15 witnesses for program sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c, ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 864a96b Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T18:41:21+01:00
Download f795473 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-11T16:59:44
Download d479fe7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-08T23:22:34
Download d48bdef Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 5 2020-12-12T01:45:48+01:00 Download f795473
Download 5f84804 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 15 2020-12-09T22:08:37+01:00 Download 1ee7f9e
Download de5caa2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 5 2020-12-09T03:57:36+01:00 Download d479fe7
Download d454df8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 15 2020-12-09T02:03:12+01:00 Download d863f95
Download fbc6889 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 15 2020-12-06T19:25:25+01:00 Download 864a96b
Download 1e1aa54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 7 2020-12-07T16:45:14+01:00 Download 41e2f90
Download 22d2a24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 15 2020-12-09T21:49:27+01:00 Download 4b5d7fe
Download 2b7a996 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 15 2020-12-08T06:36:34+01:00 Download 31fc15b
Download 5dc67c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 15 2020-12-06T18:01:20+01:00 Download 080ea9d
Download fa6506c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 15 2020-12-05T18:05:11+01:00 Download 080ea9d
Download 080ea9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 15 2020-12-05T16:02:22+01:00
Download 31fc15b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 15 2020-12-07T22:41:51+01:00

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

Trying to find witnesses for program (ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6, sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c).

Found 13 witnesses for program sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c, ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 534a08e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2019-12-01 09:47:00
Download 864b11d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 15 2019-12-11T21:42:28+01:00 Download 4c1b689
Download 130dc64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 15 2019-12-03T08:10:04+01:00 Download cffda01
Download cffda01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 15 2019-11-30T06:32:39+01:00
Download ffdbeba Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 7 2019-12-05T20:20:32+01:00 Download 95acd46
Download cc3467b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 15 2019-12-11T21:55:08+01:00 Download c0b8a8f
Download e9b453e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 5 2019-12-11T21:09:05+01:00 Download 534a08e
Download 31efc5a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 15 2019-12-08T00:27:24+01:00 Download bde8c42
Download 0ff493e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 15 2019-12-08T00:06:01+01:00 Download c3c2f34
Download cb79190 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 15 2019-12-07T21:12:42+01:00 Download 857c86b
Download d6305f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 15 2019-12-03T08:57:01+01:00 Download 594cc92
Download 73f1ccf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 15 2019-12-11T20:55:11+01:00 Download c5052bd
Download 4c1b689 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 15 2019-12-01T17:41:38+01:00

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

Trying to find witnesses for program (ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6, sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c).

Found 10 witnesses for program sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c, ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 62dd25a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 15 2018-12-09T20:53:10+01:00 Download 5b2ec9b
Download 3ea7f49 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 15 2018-12-09T20:18:12+01:00 Download 6611709
Download c3834da Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 15 2018-12-08T08:11:32+01:00 Download b702de8
Download c8883c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 15 2018-12-06T09:48:19+01:00 Download 4c0ea7f
Download 641ba23 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 15 2018-12-10T10:48:54+01:00 Download ab28e3b
Download dde12d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 15 2018-12-09T20:38:23+01:00 Download 271c821
Download 0bf476c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 15 2018-12-07T09:29:31+01:00 Download 677dd6c
Download 4c0ea7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 15 2018-12-06T02:41:22+01:00
Download b702de8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 15 2018-12-08T02:35:41+01:00
Download f4559fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 15 2018-12-08T04:33:32+01:00 Download ab28e3b

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

Trying to find witnesses for program (ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6, sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c).

Found 0 witnesses for program sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c, ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6.json

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

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

Trying to find witnesses for program (ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6, sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c).

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

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