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/memsetNonZero_false-valid-deref-write.c
programSHA e1bccb981acdddec34b38cf69d1550cfb048293e7126831a8b31b1b676fdcae7
witnessName results-verified/esbmc-incr.2017-12-02_0000.logfiles/sv-comp18.memsetNonZero_false-valid-deref-write.c.files/witness.graphml
witnessSHA 1864fd420e30cf2a1621f147ec3600391206804c389289bcda8c0139db28fd72

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/1864fd420e30cf2a1621f147ec3600391206804c389289bcda8c0139db28fd72.json

Key Value
architecture 32bit
creationtime 2017-12-01T23:51:13.282858
producer ESBMC 4.6.0 incr
program-sha256 e1bccb981acdddec34b38cf69d1550cfb048293e7126831a8b31b1b676fdcae7
programfile ../../sv-benchmarks/c/ldv-memsafety/memsetNonZero_false-valid-deref-write.c
programhash cef7b9fedda26f2b86e76703e63f684bda898c92
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) )
witness-file witnessFileByHash/1864fd420e30cf2a1621f147ec3600391206804c389289bcda8c0139db28fd72.graphml
witness-sha256 1864fd420e30cf2a1621f147ec3600391206804c389289bcda8c0139db28fd72
witness-size 3617
witness-type violation_witness

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ac3a890 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T09:52:07+01:00
Download eb0dddd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2023-12-17T00:41:17Z
Download bd8071c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2023-11-29T19:43:19Z
Download 837b3ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-19T15:33:42+01:00 Download 0c4fb5b
Download f53d88a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-19T05:28:06+01:00 Download afd1d67
Download b24e43c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-18T12:05:02+01:00 Download ac3a890
Download 863d0a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-18T03:08:59+01:00 Download 9f574e5
Download 09ca2e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-17T22:06:21+01:00 Download 16b7c8c
Download d6f2a65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-17T06:38:11+01:00 Download eb0dddd
Download d6e3033 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-05T14:40:32+01:00 Download 6c51270
Download 8f105fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-04T16:39:25+01:00 Download 102bbe8
Download 9cc9d05 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-04T02:27:13+01:00 Download 941260b
Download 40bac66 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-01T22:54:05+01:00 Download d18da85
Download f72f958 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T13:44:12+01:00 Download bb5474d
Download 74065ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T09:44:10+01:00 Download fa41687
Download bb5474d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T08:21:41+01:00
Download 52463b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T03:06:21+01:00 Download bd8071c
Download 90d777d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-28T23:49:45+01:00 Download ebfde74
Download 941260b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 3 2023-12-03T22:32:16+01:00
Download 0c4fb5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2023-12-19T13:09:08+01:00
Download 9f574e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 3 2023-12-18T02:13:06+01:00
Download 97822c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-12-04T12:12:28+01:00 Download d07a403
Download d8327df Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-12-03T06:18:19+01:00 Download d1b7cd7
Download 4ac1cbc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-12-01T18:28:06+01:00 Download d60ac4a
Download 20bc3ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-11-29T08:34:55+01:00 Download 1683b7b
Download d60ac4a 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:22:48Z
Download d07a403 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:54:04Z
Download d1b7cd7 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-03T02:44:33Z
Download 16b7c8c 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:20:33+01:00
Download 1683b7b 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-29T02:27:04Z
Download ebfde74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness sv-sanitizers 0.1.1 3 2023-11-28T22:13:02Z
Download fa41687 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2023-11-30T08:25:10Z
Download afd1d67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2023-12-19T00:51:05+01:00
Download 6c51270 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-05T10:46:31Z
Download 102bbe8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-04T14:27:19Z
Download d18da85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-01T19:58:00Z
Download a0f5534 Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow location: column: 3 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_417acdb7-e156-4182-bbf3-914e3c7a0296/sv-benchmarks/c/ldv-memsafety/memsetNonZero_-write.c line: 27 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T19:43:19Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_417acdb7-e156-4182-bbf3-914e3c7a0296/sv-benchmarks/c/ldv-memsafety/memsetNonZero_-write.c : e1bccb981acdddec34b38cf69d1550cfb048293e7126831a8b31b1b676fdcae7 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_417acdb7-e156-4182-bbf3-914e3c7a0296/sv-benchmarks/c/ldv-memsafety/memsetNonZero_-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:57:59+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0d78025 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T07:12:31+01:00
Download 99d45bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-25T11:52:26Z
Download a76f53b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-12T15:17:58Z
Download 06cb28a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T05:56:11+01:00 Download a76f53b
Download a159a0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T04:19:11+01:00 Download 476c694
Download 1b0610e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T01:32:17+01:00 Download 56aeedd
Download 30463b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T00:54:01+01:00 Download f9c208e
Download 0440256 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T21:06:49+01:00 Download 97f66d7
Download f9806f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T14:09:48+01:00 Download 0d78025
Download c98c5c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T08:56:15+01:00 Download cdd58de
Download 082daba Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T06:01:31+01:00 Download 51b6793
Download c429156 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T04:22:07+01:00 Download 6aec860
Download 1adf276 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T02:23:57+01:00 Download 99d45bf
Download 2070360 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T00:27:59+01:00 Download 7fad1ae
Download cdd58de Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2022-12-10T19:27:25+01:00
Download 56aeedd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 3 2022-12-11T23:10:39+01:00
Download 97f66d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2022-12-10T02:20:07+01:00
Download 51b6793 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 3 2022-12-09T02:47:39+01:00
Download 80c1925 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-29T10:44:10+01:00 Download 6312003
Download 7b74de2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-29T06:52:41+01:00 Download 77f1dd6
Download 40ba8be Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-29T06:38:44+01:00 Download a122dc3
Download 62afbc1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-28T15:45:13+01:00 Download 3a95323
Download 3a95323 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.0.0 incr 4 2022-12-18T19:19:13Z
Download 6312003 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-14T05:51:47Z
Download a122dc3 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-14T22:37:04Z
Download 6aec860 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-08T10:03:46+01:00
Download 77f1dd6 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-13T16:09:19Z
Download f9c208e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2022-12-11T02:10:44+01:00
Download 7fad1ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2022-12-08T18:57:42Z

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0566baf Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T09:15:03+01:00
Download 1dfa180 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2021-12-10T19:09:09
Download e79eafe Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2021-12-07T15:09:18Z
Download 9b037de Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-10T21:29:02+01:00 Download 1dfa180
Download f4d7d61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-09T16:03:28+01:00 Download 898fa28
Download f3cb45b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-09T06:21:41+01:00 Download 476c694
Download f095f4f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-08T21:07:38+01:00 Download 9ed6689
Download 2f5b0d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T19:10:42+01:00 Download e79eafe
Download 6fcc147 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T11:27:51+01:00 Download 0566baf
Download 4db31bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T04:55:20+01:00 Download 15ab98e
Download 100d8f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-06T11:48:32+01:00 Download 3c49b71
Download 0ef9ea3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-05T20:41:32+01:00 Download 7920d35
Download 7920d35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-05T16:35:41+01:00
Download 898fa28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2021-12-09T13:38:37+01:00
Download 15ab98e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 3 2021-12-07T01:57:41+01:00
Download f2fa505 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-10T17:27:05+01:00 Download 33d4f38
Download 4b4f4fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-10T08:33:20+01:00 Download 6eaee37
Download eed1c9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-08T13:46:31+01:00 Download 289dabf
Download 7c16ac8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-07T02:34:54+01:00 Download cc7beba
Download 289dabf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2021-12-08T06:38:26Z
Download 6eaee37 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-10T02:28:28Z
Download 33d4f38 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-10T15:28:13Z
Download 3c49b71 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 2021-12-06T02:08:55+01:00
Download cc7beba 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-07T00:03:39Z
Download 9ed6689 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 3 2021-12-08T17:45:24+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 11308da Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T12:02:54+01:00
Download e1c1b21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-11T19:32:51
Download 9799315 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-09T01:10:52
Download ad6e715 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-12T01:38:40+01:00 Download e1c1b21
Download 2c55628 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-09T21:49:42+01:00 Download cdb7ea1
Download 8d94533 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-09T21:43:12+01:00 Download 973bcc2
Download f1e85a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-09T04:11:50+01:00 Download 9799315
Download d736055 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-08T06:35:39+01:00 Download 1868975
Download b3f147d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-06T18:27:32+01:00 Download 83dbb6b
Download e5e7902 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-06T18:01:38+01:00 Download 849d7f1
Download 5a5733f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-06T07:40:42+01:00 Download 83dbb6b
Download 7b46dce Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-05T18:49:29+01:00 Download 849d7f1
Download 849d7f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-05T14:48:02+01:00
Download 1868975 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2020-12-08T04:58:49+01:00
Download 7159f29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-09T02:08:28+01:00 Download 8b45f78
Download a0defcf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-06T18:59:43+01:00 Download 11308da
Download 75e6fec Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0 3 2020-12-07T16:23:40+01:00 Download 0390139

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d370090 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2019-12-01 08:17:55
Download 365c739 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:55:54+01:00 Download 1836263
Download ee04ca1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:45:05+01:00 Download 3a0e509
Download b7cd9bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:09:05+01:00 Download d370090
Download b845bb7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-08T00:06:03+01:00 Download 476c694
Download 3384d55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-06T02:38:42+01:00 Download e2e8c0c
Download 0005c9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-05T20:21:50+01:00 Download 057aa5f
Download 66ef6bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-03T08:57:05+01:00 Download 5a60021
Download f6bd0fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-11-30T06:44:03+01:00
Download 4560160 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 3 2019-12-08T00:26:27+01:00 Download 203c929
Download 4028af3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 3 2019-12-07T21:16:43+01:00 Download 2c799b5
Download 3a0e509 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 3 2019-12-01T12:46:52+01:00
Download feafb48 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 3 2019-12-11T20:54:46+01:00 Download c3fbefe
Download 88a995f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 3 2019-12-03T08:07:37+01:00 Download f6bd0fd

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 9b94744 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T07:02 CET (sv-comp)
Download 4527c4b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:22:27+01:00 Download 3845d9a
Download 9dc4a8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T23:43:58+01:00 Download 9b94744
Download c0cecf1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T08:47:27+01:00 Download f18749f
Download 52664af Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:16:59+01:00 Download 52d5fdf
Download 1d77960 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T03:19:22+01:00
Download 342215b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-06T10:18:03+01:00 Download 463bb75
Download f18749f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 3 2018-12-07T23:27:56+01:00
Download 22f411b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-10T10:48:48+01:00 Download bb35bf0
Download 6005d96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:53:07+01:00 Download 5b955ed
Download 23e90b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T22:07:24+01:00 Download f5c8275
Download 057c469 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-07T09:27:03+01:00 Download e64e6ee
Download e67a2f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:48:00+01:00 Download 1d77960
Download f5c8275 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-08T12:26:25
Download acfb326 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:39:28+01:00 Download 5387be7
Download 513fcf7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T03:38:43+01:00 Download bb35bf0
Download 0c92b0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:18:05+01:00 Download 7ad9e0e
Download 1371aa0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-08T05:02:11+01:00 Download 576f7ba

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0bc8828 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-02T23:43 CET (sv-comp)
Download 6adbcf2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.6.1-svn 26773 3 2017-12-01T08:28:19+01:00
Download c03a9bc 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:21:49.779166
Download 1864fd4 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:51:13.282858
Download db10baf 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:55Z
Download 46fbbd6 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-03T03:42Z
Download 0afea7a 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 Forester 4 2017-12-01T19:49 CET (sv-comp)
Download 3b5b94f 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:29 CET (sv-comp)
Download a4d48ef 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 3 2017-12-03T03:43Z
Download e64e6ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2017-12-01T21:56 CET (sv-comp)
Download 3e57dee Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Map2Check 2 2017-12-01T23:46 CET (sv-comp)

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

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

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

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