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/memset3_false-valid-deref-write.c
programSHA 4f4c34e89258ad08f5ff0f3cdaddc883f4834617a4558e66914b1b5dcd1f7778
witnessName results-verified/uautomizer.2018-12-08_0742.logfiles/sv-comp19_prop-memsafety.memset3_false-valid-deref-write.c.files/witness.graphml
witnessSHA cc6ffca19f6240b4f7d005c269be5cba9952c0ba2445f0c6e9d84f202acedad4

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-08T08:11Z
error-specification-length Key 'specification' longer than 100 characters.
producer Automizer
programfile /tmp/vcloud-vcloud-master/worker/working_dir_7eb0855d-44b6-4f47-9b01-af78907cd186/sv-benchmarks/c/ldv-memsafety/memset3_false-valid-deref-write.c
programhash 97106d24c91338d3a7f71605e6dcf95bdff73f56
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )
witness-file witnessFileByHash/cc6ffca19f6240b4f7d005c269be5cba9952c0ba2445f0c6e9d84f202acedad4.graphml
witness-sha256 cc6ffca19f6240b4f7d005c269be5cba9952c0ba2445f0c6e9d84f202acedad4
witness-size 3883
witness-type violation_witness

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a657cd3 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T09:58:50+01:00
Download 57d2eed Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2023-12-17T01:59:44Z
Download 73b1225 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2023-11-29T19:28:53Z
Download 94122bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-19T15:32:25+01:00 Download f2d89c2
Download 87f6149 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-19T05:26:36+01:00 Download 40e76a0
Download c53644f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-18T12:04:45+01:00 Download a657cd3
Download a6cdfac Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-18T03:09:22+01:00 Download 9ac92d9
Download c320eb7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-17T22:09:07+01:00 Download bd3593b
Download 737e989 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-17T06:41:21+01:00 Download 57d2eed
Download 2e48b30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-05T14:40:49+01:00 Download 9898ae2
Download 145cdf4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-04T16:42:37+01:00 Download 433911a
Download 0c3adfd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-04T02:25:52+01:00 Download 2896c39
Download 0512a5a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-01T22:56:19+01:00 Download bfdf60e
Download 6630a7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T13:43:50+01:00 Download f8e1da8
Download 4e2c503 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T09:44:00+01:00 Download 9c2d420
Download f8e1da8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T06:04:17+01:00
Download d1678f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T03:03:37+01:00 Download 73b1225
Download 969d589 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-28T23:50:04+01:00 Download bbef4fc
Download 2896c39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 3 2023-12-04T00:16:58+01:00
Download f2d89c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2023-12-19T13:08:50+01:00
Download 40e76a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2023-12-18T19:49:28+01:00
Download 9ac92d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 4 2023-12-18T01:49:00+01:00
Download 12f17f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-12-04T12:12:26+01:00 Download 8b37ebf
Download 457c801 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-12-03T06:19:25+01:00 Download 6d3c842
Download 73d1b90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-12-01T18:26:49+01:00 Download 7efbb4e
Download ef09ec5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-11-29T08:33:20+01:00 Download 2741589
Download 7efbb4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.4.0 incr 4 2023-12-01T15:38:32Z
Download 8b37ebf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Taipan 4 2023-12-02T12:46:20Z
Download 6d3c842 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Kojak 4 2023-12-03T00:34:10Z
Download bd3593b 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-17T15:05:13+01:00
Download 2741589 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Automizer 4 2023-11-28T23:51:27Z
Download bbef4fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness sv-sanitizers 0.1.1 3 2023-11-28T22:24:38Z
Download 9c2d420 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2023-11-30T08:25:30Z
Download 9898ae2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-05T11:04:57Z
Download 433911a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-04T09:05:30Z
Download bfdf60e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-01T21:17:54Z
Download e9f59f6 Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow location: column: 3 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a406f42a-2e1f-44c5-b528-1d62b6120bc3/sv-benchmarks/c/ldv-memsafety/memset3_-write.c line: 29 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T19:28:53Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a406f42a-2e1f-44c5-b528-1d62b6120bc3/sv-benchmarks/c/ldv-memsafety/memset3_-write.c : 4f4c34e89258ad08f5ff0f3cdaddc883f4834617a4558e66914b1b5dcd1f7778 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a406f42a-2e1f-44c5-b528-1d62b6120bc3/sv-benchmarks/c/ldv-memsafety/memset3_-write.c language: C specification: CHECK( init(main()), LTL(G valid-free) ),CHECK( init(main()), LTL(G valid-deref) ),CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 4 2023-11-30T02:56:44+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download bedbfd0 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T07:10:53+01:00
Download f87b5e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-25T10:19:59Z
Download 50b1de3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-12T17:41:47Z
Download e898c8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T05:57:46+01:00 Download 50b1de3
Download 619b778 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T04:19:19+01:00 Download 0cdd984
Download fac2e29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T01:32:20+01:00 Download defcdda
Download cc174fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T00:54:31+01:00 Download 6137e22
Download 4fc0350 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T21:06:26+01:00 Download 7863901
Download dbd1dff Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T14:17:57+01:00 Download bedbfd0
Download 7c0ebbd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T08:58:42+01:00 Download 13ea19c
Download a7036d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T06:01:29+01:00 Download dd069b1
Download efd5ecb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T04:21:37+01:00 Download b142ff5
Download 5002f14 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T02:24:06+01:00 Download f87b5e4
Download 4d8008b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T00:29:32+01:00 Download c9c1cb5
Download 13ea19c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2022-12-10T20:21:55+01:00
Download defcdda Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 3 2022-12-11T23:34:27+01:00
Download 7863901 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2022-12-10T04:24:16+01:00
Download dd069b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 4 2022-12-09T03:03:25+01:00
Download 546cd71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-29T10:44:39+01:00 Download f997bd6
Download 3777b29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-29T06:52:56+01:00 Download 2b2cf5e
Download 57bd4f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-29T06:38:28+01:00 Download 2db4745
Download 567fc97 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-28T15:45:37+01:00 Download 2b0d140
Download 2b0d140 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.0.0 incr 4 2022-12-18T23:07:50Z
Download f997bd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Taipan 4 2022-12-14T12:42:19Z
Download 2db4745 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Kojak 4 2022-12-15T00:33:18Z
Download b142ff5 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-08T13:05:35+01:00
Download 2b2cf5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Automizer 4 2022-12-13T21:21:42Z
Download 6137e22 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2022-12-11T04:38:46+01:00
Download c9c1cb5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2022-12-08T14:53:52Z

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 63ba42c Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T08:01:58+01:00
Download a25a8f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2021-12-10T18:10:07
Download c0bae54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2021-12-07T15:13:54Z
Download c861735 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-10T21:26:56+01:00 Download a25a8f3
Download e0617a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-09T16:02:25+01:00 Download 182454f
Download 2732d06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-09T06:21:52+01:00 Download 0cdd984
Download 1b73b84 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-08T21:06:33+01:00 Download 241d28a
Download f9ab0db Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T19:12:33+01:00 Download c0bae54
Download 49d69f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T11:27:45+01:00 Download 63ba42c
Download 1217646 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T04:56:30+01:00 Download 9dd5bca
Download e098c5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-06T11:48:08+01:00 Download a878d1e
Download 38a5190 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-05T20:39:05+01:00 Download f149055
Download f149055 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-05T18:13:41+01:00
Download 182454f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2021-12-09T14:10:55+01:00
Download 9dd5bca Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 4 2021-12-07T02:03:11+01:00
Download 0a05ee9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-10T17:27:08+01:00 Download 6f2adbd
Download 017dee8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-10T08:34:10+01:00 Download a4093b5
Download f26f4d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-08T13:50:18+01:00 Download d1ad56a
Download fb0067f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-07T02:35:39+01:00 Download 7e5169c
Download d1ad56a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2021-12-08T04:07:51Z
Download a4093b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Taipan 4 2021-12-09T22:53:33Z
Download 6f2adbd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Kojak 4 2021-12-10T13:38:55Z
Download a878d1e 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-06T05:15:12+01:00
Download 7e5169c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Automizer 4 2021-12-06T23:26:21Z
Download 241d28a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 3 2021-12-08T20:15:04+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 845017a Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T18:43:43+01:00
Download c6d48e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-11T20:09:19
Download ecdef01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-08T20:10:28
Download 7bd6e34 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-12T01:30:51+01:00 Download c6d48e6
Download a4c92bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-09T22:03:30+01:00 Download a9df05b
Download 81cd192 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-09T21:37:00+01:00 Download 9044daa
Download d36c2c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-09T04:11:10+01:00 Download ecdef01
Download a2c5c9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-08T06:27:34+01:00 Download 4c3ee5e
Download eca7266 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-06T19:25:36+01:00 Download 845017a
Download 2a569ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-06T18:27:03+01:00 Download 12d20ea
Download 16c2928 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-05T18:24:54+01:00 Download 3deddbf
Download 4c3ee5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2020-12-08T01:23:43+01:00
Download f4fd4d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 3 2020-12-07T16:32:01+01:00 Download 2e48f79
Download 5666beb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 3 2020-12-09T02:30:29+01:00 Download 0262057
Download bd686ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 3 2020-12-06T18:01:15+01:00 Download 3deddbf
Download 61ee6b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-06T07:55:06+01:00 Download 12d20ea
Download 3deddbf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-05T16:55:16+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4dc144d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2019-12-01 23:41:08
Download 92f5574 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:45:31+01:00 Download ec0b59f
Download a446cad Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:09:23+01:00 Download 4dc144d
Download 1486414 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-08T00:06:05+01:00 Download 0cdd984
Download 4f83e04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-07T21:15:37+01:00 Download 710c9d5
Download 87c15cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-06T02:40:16+01:00 Download cfe73b3
Download 8aff569 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-05T20:20:13+01:00 Download 1ee8e9d
Download 94d7607 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-03T08:57:58+01:00 Download 8142b2f
Download 48d246b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-03T08:10:32+01:00 Download 61e3971
Download 61e3971 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-11-29T15:56:58+01:00
Download ec0b59f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 3 2019-12-01T00:13:21+01:00
Download 17019cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 3 2019-12-11T20:54:48+01:00 Download 0dffc50
Download 25dc692 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:58:38+01:00 Download c89f35b
Download 9d8444d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 3 2019-12-08T00:27:07+01:00 Download 45a13a0

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ee91291 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T10:00 CET (sv-comp)
Download 0e2c7db Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:39:27+01:00 Download cc6ffca
Download c7a7e84 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T22:08:43+01:00 Download bcfafb0
Download afbfad9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:17:48+01:00 Download 95815db
Download 1e641fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:17:44+01:00 Download 1da0ebd
Download 054dfc9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T06:23:49+01:00
Download 009ab57 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-08T05:01:32+01:00 Download d2fa7ff
Download 9766d7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:33:56+01:00 Download 8950dc1
Download de9f732 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T07:48:34+01:00 Download 42939bf
Download fa99517 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-07T09:27:39+01:00 Download 5da882d
Download 0aa778f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:47:54+01:00 Download 054dfc9
Download e43a751 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-06T10:18:25+01:00 Download fc13e3b
Download bcfafb0 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-07T21:40:08
Download 42939bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 3 2018-12-07T14:46:18+01:00
Download 2d9282f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-10T10:48:55+01:00 Download b173d6d
Download 00dcd65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:53:25+01:00 Download 5b473e8
Download 8399110 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T23:44:51+01:00 Download ee91291
Download f737376 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T03:42:48+01:00 Download b173d6d

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

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

Found 10 witnesses for program sv-benchmarks/c/ldv-memsafety/memset3_false-valid-deref-write.c, 4f4c34e89258ad08f5ff0f3cdaddc883f4834617a4558e66914b1b5dcd1f7778
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/4f4c34e89258ad08f5ff0f3cdaddc883f4834617a4558e66914b1b5dcd1f7778.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7fc6c06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-02T23:12 CET (sv-comp)
Download 5929339 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.6.1-svn 26773 3 2017-12-01T08:32:50+01:00
Download 3faf943 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:53:58.375315
Download 17d568e 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:43:33.397765
Download 83cdf12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Taipan 4 2017-12-03T06:54Z
Download 4a859e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Kojak 4 2017-12-03T04:14Z
Download b1497e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CBMC 4 2017-12-01T08:25 CET (sv-comp)
Download 7a13a96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Automizer 4 2017-12-03T04:16Z
Download 5da882d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2017-12-01T22:06 CET (sv-comp)
Download a902e3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Map2Check 3 2017-12-01T23:29 CET (sv-comp)

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

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

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

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