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/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c
programSHA 9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b
witnessName results-verified/pesco.2018-12-06_1244.logfiles/sv-comp19_prop-memsafety.ArraysWithLenghtAtDeclaration_false-valid-deref-read.c.files/witness.graphml
witnessSHA 9c3ac3c7ca109f9437b2d0da293b2b1e956ee03804e11e639dc1e2e9d03ba13e

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-07T10:25:29+01:00
producer CPAchecker 1.7-svn b8d6131600+
program-sha256 9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b
programfile ../../sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c
programhash 9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-deref) )
witness-file witnessFileByHash/9c3ac3c7ca109f9437b2d0da293b2b1e956ee03804e11e639dc1e2e9d03ba13e.graphml
witness-sha256 9c3ac3c7ca109f9437b2d0da293b2b1e956ee03804e11e639dc1e2e9d03ba13e
witness-size 601238
witness-type violation_witness

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

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

Trying to find witnesses for program (9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b, sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c).

Found 29 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c, 9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7e6e694 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T10:55:33+01:00
Download 2743160 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2023-11-29T23:27:06Z
Download ff16e92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 600 2023-12-19T05:27:09+01:00 Download 6069f59
Download 6a0bb80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 601 2023-12-18T12:02:48+01:00 Download 7e6e694
Download 2e7891b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 600 2023-12-18T03:09:11+01:00 Download e5deb10
Download f4be45e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 600 2023-12-17T22:09:28+01:00 Download 8fa4588
Download 3c54228 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 601 2023-12-05T14:39:52+01:00 Download c582a3f
Download e12fedb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 601 2023-12-04T16:44:16+01:00 Download ed9ceaf
Download 23dae86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 600 2023-12-04T12:13:51+01:00 Download 4a1c121
Download e34b2dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 600 2023-12-04T02:25:22+01:00 Download a55c790
Download 0dc23cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 601 2023-12-01T22:54:22+01:00 Download a290f75
Download 3ec1f12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 600 2023-12-01T18:29:01+01:00 Download 5e7e586
Download 0e86d42 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 600 2023-11-30T13:45:25+01:00 Download c367624
Download f020218 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 600 2023-11-30T09:44:06+01:00 Download 1d26ddc
Download c367624 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 481 2023-11-30T08:38:15+01:00
Download 274d159 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 601 2023-11-30T03:03:09+01:00 Download 2743160
Download 57a4fe2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 601 2023-11-28T23:49:54+01:00 Download d0ad74d
Download a55c790 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 601 2023-12-03T21:55:28+01:00
Download e5deb10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 940 2023-12-18T01:36:16+01:00
Download 5e7e586 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:39:51Z
Download 4a1c121 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 561 2023-12-02T15:55:00Z
Download 8fa4588 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-17T11:37:58+01:00
Download d0ad74d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness sv-sanitizers 0.1.1 3 2023-11-28T20:32:39Z
Download 1d26ddc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 13 2023-11-30T08:25:20Z
Download 6069f59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 601 2023-12-18T16:32:48+01:00
Download c582a3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-05T07:45:23Z
Download ed9ceaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-04T12:48:01Z
Download a290f75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-01T20:04:15Z
Download 140c25a Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow location: column: 6 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c6f9ca8e-1150-471c-ac1a-7666cd2f8ea7/sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_-read.c line: 18 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T23:27:06Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c6f9ca8e-1150-471c-ac1a-7666cd2f8ea7/sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_-read.c : 9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c6f9ca8e-1150-471c-ac1a-7666cd2f8ea7/sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_-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 601 2023-11-30T02:57:19+01:00

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

Trying to find witnesses for program (9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b, sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c).

Found 23 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c, 9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fa0b2d8 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T07:13:59+01:00
Download 76a99da Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-12T13:02:22Z
Download b43d4a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 601 2023-01-29T10:44:13+01:00 Download 2ca9f55
Download b50df08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 601 2023-01-29T05:58:45+01:00 Download 76a99da
Download 764b468 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 601 2023-01-29T04:19:26+01:00 Download 24dedc9
Download 09bea55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 601 2023-01-29T01:31:56+01:00 Download a1e6749
Download bb07df5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 601 2023-01-28T21:08:33+01:00 Download 8b4d17c
Download 7ef583f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 601 2023-01-28T15:45:41+01:00 Download 15aaea3
Download 2c07ea9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 601 2023-01-28T14:15:29+01:00 Download fa0b2d8
Download 1bd2ab0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 601 2023-01-28T08:58:25+01:00 Download 3d44429
Download 1f59375 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 601 2023-01-28T06:01:32+01:00 Download d172184
Download 0308525 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 601 2023-01-28T04:21:27+01:00 Download 57e562c
Download 2ad7b73 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 601 2023-01-28T02:24:39+01:00 Download 85d686b
Download e2bf0ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 601 2023-01-28T00:29:31+01:00 Download 45e56b8
Download 3d44429 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 601 2022-12-10T19:44:00+01:00
Download a1e6749 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 601 2022-12-12T01:01:02+01:00
Download d172184 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 940 2022-12-09T03:01:42+01:00
Download 15aaea3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.0.0 incr 4 2022-12-19T00:38:53Z
Download 85d686b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2022-12-25T12:32:51Z
Download 8b4d17c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 601 2022-12-10T01:45:51+01:00
Download 2ca9f55 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 545 2022-12-14T09:35:33Z
Download 57e562c 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-08T13:24:36+01:00
Download 45e56b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2022-12-08T20:22:23Z

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

Trying to find witnesses for program (9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b, sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c).

Found 24 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c, 9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 28bb2d9 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T09:23:55+01:00
Download c3a367e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2021-12-10T16:20:01
Download ea449ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2021-12-07T13:53:37Z
Download ee40a10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 601 2021-12-10T21:25:46+01:00 Download 734c680
Download 99e0928 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 601 2021-12-10T08:34:22+01:00 Download 210d72f
Download c1f8a86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 601 2021-12-09T16:03:35+01:00 Download b8de19f
Download a818dc7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 601 2021-12-09T06:21:43+01:00 Download 24dedc9
Download 69126fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 601 2021-12-08T21:10:55+01:00 Download e2b4668
Download e3c58a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 601 2021-12-08T13:46:57+01:00 Download 3c8b30e
Download e992683 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 601 2021-12-07T19:10:31+01:00 Download ea449ac
Download d9483eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 601 2021-12-07T11:25:42+01:00 Download 28bb2d9
Download 143a7a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 601 2021-12-07T04:55:59+01:00 Download 629a7eb
Download cde2a0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 601 2021-12-07T02:34:51+01:00 Download 84acede
Download fed5fef Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 601 2021-12-05T20:40:13+01:00 Download f1bfa10
Download f1bfa10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 601 2021-12-05T17:34:19+01:00
Download 629a7eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 940 2021-12-07T02:16:19+01:00
Download 44434a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 8 2021-12-06T11:47:45+01:00 Download df65afa
Download 3c8b30e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2021-12-08T05:25:36Z
Download 210d72f 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 545 2021-12-10T04:47:47Z
Download df65afa 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 446 2021-12-06T07:53:23+01:00
Download 84acede 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 546 2021-12-06T23:12:48Z
Download 697ae78 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness SESL 2 2021-12-06T11:22:00+01:00
Download e2b4668 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 601 2021-12-08T19:27:37+01:00
Download b8de19f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 601 2021-12-09T11:08:30+01:00

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

Trying to find witnesses for program (9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b, sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c).

Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c, 9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ba8b501 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T17:54:25+01:00
Download 98030fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-11T15:21:15
Download 49ad572 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-08T18:54:22
Download d9cdda3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 601 2020-12-12T01:38:17+01:00 Download 98030fa
Download c17cc27 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 601 2020-12-09T04:11:59+01:00 Download 49ad572
Download c02d6b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 601 2020-12-07T16:09:32+01:00 Download 90c5ecd
Download 9c48fed Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 601 2020-12-06T18:01:21+01:00 Download 2159a94
Download 2159a94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 601 2020-12-05T12:49:24+01:00
Download e26b42e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 601 2020-12-08T04:00:50+01:00
Download 24dbb41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 9 2020-12-06T18:26:57+01:00 Download b90be41
Download 4c6f7c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 9 2020-12-06T07:41:22+01:00 Download b90be41
Download 5b8806e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 601 2020-12-08T07:52:31+01:00 Download e26b42e
Download b0b1cb6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 601 2020-12-06T19:09:57+01:00 Download ba8b501
Download 3da464f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 601 2020-12-05T17:45:26+01:00 Download 2159a94

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

Trying to find witnesses for program (9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b, sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c).

Found 13 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c, 9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 632ceba Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2019-12-01 14:12:23
Download a09a53b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 601 2019-12-11T20:55:11+01:00 Download bc46e66
Download 43826cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 601 2019-12-07T21:18:51+01:00 Download 88c5cd2
Download 45d5e00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 601 2019-12-06T02:38:39+01:00 Download 3c520b3
Download ea613e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 601 2019-12-03T08:10:40+01:00 Download c9c6f89
Download d15be69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 601 2019-12-01T00:16:37+01:00
Download 4770199 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 601 2019-12-11T21:43:25+01:00 Download d15be69
Download f153843 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 601 2019-12-03T08:56:59+01:00 Download 5b1f2f3
Download b31ca96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 8 2019-12-05T20:21:05+01:00 Download 4f02c11
Download ace5bbb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 601 2019-12-11T21:09:29+01:00 Download 632ceba
Download 3238fa7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 601 2019-12-08T00:26:18+01:00 Download 3cc623a
Download c55e030 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 601 2019-12-08T00:07:06+01:00 Download 24dedc9
Download c9c6f89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 601 2019-11-30T13:17:32+01:00

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

Trying to find witnesses for program (9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b, sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c).

Found 16 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c, 9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 53c15d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T01:13 CET (sv-comp)
Download afc722c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 601 2018-12-10T10:48:48+01:00 Download 6e0c0dd
Download 1d6c746 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 601 2018-12-09T20:53:32+01:00 Download 95d6f96
Download 98f8216 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 601 2018-12-09T20:34:19+01:00 Download 35e627d
Download 184db0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 601 2018-12-08T08:30:31+01:00 Download 9c3ac3c
Download 2939a81 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 601 2018-12-06T09:49:02+01:00 Download f829aad
Download f829aad Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 601 2018-12-05T14:49:28+01:00
Download 4ef6873 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:16:44+01:00 Download b74ad3b
Download 26190a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 601 2018-12-07T09:18:58+01:00 Download 8e2f9ca
Download 9c3ac3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 601 2018-12-07T10:25:29+01:00
Download 5ccc3b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 601 2018-12-08T23:44:45+01:00 Download 53c15d5
Download d62d95f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 601 2018-12-08T05:06:28+01:00 Download efe7932
Download 95eeed3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 601 2018-12-08T04:03:36+01:00 Download 6e0c0dd
Download 15f2882 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 601 2018-12-07T01:19:40+01:00 Download 41a14bc
Download d4d5c24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 601 2018-12-06T10:19:10+01:00 Download b8a4edf
Download 3d64258 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:20:28+01:00 Download 79f8d0e

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

Trying to find witnesses for program (9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b, sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c).

Found 9 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c, 9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0bebf13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-02T23:13 CET (sv-comp)
Download d47d1d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.6.1-svn 26773 546 2017-12-01T08:34:16+01:00
Download 9f5de4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T11:04:22.679817
Download 357819d 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:44:44.787599
Download 9d47745 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 3.1 145 2017-12-01T09:31 CET (sv-comp)
Download 5a06140 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 656 2017-12-01T08:27 CET (sv-comp)
Download 86a7ba2 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 2LS 469 2017-12-01T08:22 CET (sv-comp)
Download 8e2f9ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 13 2017-12-01T22:14 CET (sv-comp)
Download 1f78256 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Map2Check 4 2017-12-01T23:34 CET (sv-comp)

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

Trying to find witnesses for program (9aaf3ef5b6218ff6658a67703b1e3ffb0d16a40e5e7c9a13354b853d6f63747b, sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c).

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

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