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).

This link does not point to a witness, but below is a list of witnesses for the same program.

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

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

Found 35 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero2_false-valid-deref-write.c, 6ee5bab22bb27b31bdc1e46b5ad945cfa92016e1139565f86ec528ca863209ee
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/6ee5bab22bb27b31bdc1e46b5ad945cfa92016e1139565f86ec528ca863209ee.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 14025b5 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T10:52:52+01:00
Download 8345726 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2023-11-29T23:55:00Z
Download 2c3b2d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-19T15:33:31+01:00 Download 08e3b30
Download 3a2cd7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-19T05:27:59+01:00 Download 4961e36
Download 5734ffb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-18T12:06:57+01:00 Download 14025b5
Download f16857a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-18T03:09:24+01:00 Download edf2515
Download 45fe890 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-17T22:10:02+01:00 Download 5ba7675
Download 8add923 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-05T14:36:57+01:00 Download 15ad61a
Download b43c49e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-04T16:46:15+01:00 Download 709be9f
Download a76278d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-04T02:26:49+01:00 Download 4ed7a83
Download d225cd2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-01T22:53:32+01:00 Download 5f61fd5
Download 7d8cfbd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T13:44:07+01:00 Download 185818d
Download 7305c7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T09:44:11+01:00 Download 2a27592
Download 185818d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T06:52:03+01:00
Download e6d6a2b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T03:02:06+01:00 Download 8345726
Download 1cbe852 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-28T23:49:34+01:00 Download 8e33992
Download 4ed7a83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 3 2023-12-03T23:10:33+01:00
Download edf2515 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 3 2023-12-18T02:16:26+01:00
Download 3f29225 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-12-04T12:13:58+01:00 Download 46bfa01
Download c6c018e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-12-03T06:18:55+01:00 Download a94ef9d
Download 5992a8f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-12-01T18:29:32+01:00 Download 57bd539
Download f0b614c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-11-29T08:33:57+01:00 Download 44093e4
Download 57bd539 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:01:45Z
Download 4961e36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2023-12-18T18:38:06+01:00
Download 46bfa01 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-02T18:18:08Z
Download a94ef9d 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-03T01:50:25Z
Download 5ba7675 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-17T11:32:06+01:00
Download 44093e4 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-29T01:53:05Z
Download 8e33992 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness sv-sanitizers 0.1.1 3 2023-11-28T19:49:40Z
Download 2a27592 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2023-11-30T08:23:42Z
Download 08e3b30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2023-12-19T11:31:45+01:00
Download 15ad61a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-05T08:44:27Z
Download 709be9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-04T13:27:10Z
Download 5f61fd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-01T19:58:26Z
Download 54b16a2 Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow location: column: 3 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_cb3e2dfe-2793-4a18-8172-8df2ef60bd8a/sv-benchmarks/c/ldv-memsafety/memsetNonZero2_-write.c line: 22 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T23:55:00Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_cb3e2dfe-2793-4a18-8172-8df2ef60bd8a/sv-benchmarks/c/ldv-memsafety/memsetNonZero2_-write.c : 6ee5bab22bb27b31bdc1e46b5ad945cfa92016e1139565f86ec528ca863209ee input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_cb3e2dfe-2793-4a18-8172-8df2ef60bd8a/sv-benchmarks/c/ldv-memsafety/memsetNonZero2_-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-30T03:00:09+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download cf99d25 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T05:12:05+01:00
Download c6a6fc4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-12T12:41:27Z
Download 7e42ffc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T05:56:13+01:00 Download c6a6fc4
Download 5e55c01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T04:19:23+01:00 Download cb646d4
Download c66e2be Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T01:30:25+01:00 Download 6400df1
Download 3608aab Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T00:51:58+01:00 Download c584973
Download b490f78 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T21:05:04+01:00 Download e331f06
Download 2094fc1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T14:15:54+01:00 Download cf99d25
Download bcd5d5a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T08:56:53+01:00 Download ed0b941
Download 98241ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T06:01:21+01:00 Download 53f6088
Download 0fcae52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T04:22:09+01:00 Download f56c3c1
Download 9dfa2b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T00:29:01+01:00 Download 6fe1118
Download ed0b941 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2022-12-10T19:18:59+01:00
Download 6400df1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 3 2022-12-11T20:56:12+01:00
Download c584973 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2022-12-11T05:38:42+01:00
Download 53f6088 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 3 2022-12-09T02:17:22+01:00
Download 680a95a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-29T10:43:37+01:00 Download 8ea4e2a
Download 1e9cb24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-29T06:54:32+01:00 Download ae6ca79
Download bdb85c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-29T06:38:24+01:00 Download 481e654
Download 3f2b9ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-28T15:43:46+01:00 Download c71f9ef
Download de3f02a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-28T02:24:40+01:00 Download af4a154
Download c71f9ef 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:16:23Z
Download af4a154 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2022-12-25T10:29:54Z
Download e331f06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2022-12-10T02:31:32+01:00
Download 8ea4e2a 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-14T04:50:58Z
Download 481e654 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-14T21:15:03Z
Download f56c3c1 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-08T06:25:47+01:00
Download ae6ca79 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-13T19:02:18Z
Download 6fe1118 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2022-12-08T19:00:45Z

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 96e74c5 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T08:11:09+01:00
Download f0d5caf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2021-12-10T17:48:24
Download da19b08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2021-12-07T09:17:52Z
Download 531c4b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-10T21:28:55+01:00 Download f0d5caf
Download c5fbb89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-09T15:59:02+01:00 Download 70646a5
Download 0a1ac97 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-09T06:22:01+01:00 Download cb646d4
Download 70abd32 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-08T21:06:56+01:00 Download 875229f
Download 2ca0344 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T19:10:06+01:00 Download da19b08
Download 6676e1a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T11:28:02+01:00 Download 96e74c5
Download 7ebe82b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T04:55:16+01:00 Download d6e78b2
Download e1f8d51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-06T11:49:30+01:00 Download ffa921c
Download cbfcc69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-05T20:41:34+01:00 Download 637ac4d
Download 637ac4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-05T15:21:05+01:00
Download 875229f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 3 2021-12-08T19:31:07+01:00
Download d6e78b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 3 2021-12-07T02:10:31+01:00
Download 617fbde Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-10T17:27:26+01:00 Download 5bf484e
Download f0c0123 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-10T08:33:04+01:00 Download 55548ed
Download 158f418 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-08T13:48:41+01:00 Download b98910e
Download dee8c1d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-07T02:34:58+01:00 Download 89f231e
Download b98910e 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:35:42Z
Download 55548ed 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-10T00:03:09Z
Download 5bf484e 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-10T09:05:40Z
Download ffa921c 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-06T04:15:38+01:00
Download 89f231e 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-06T22:17:13Z
Download 70646a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2021-12-09T14:19:00+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 9989d9f Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T12:16:53+01:00
Download 11f4c86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-11T18:37:48
Download cedd224 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-08T16:30:52
Download 60cdd61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-12T01:25:37+01:00 Download 11f4c86
Download 27dea81 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-09T21:25:18+01:00 Download 8e85914
Download 93e9587 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-06T19:03:47+01:00 Download 9989d9f
Download 2e88647 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-06T18:00:38+01:00 Download a2114c0
Download bebd1af Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-06T07:39:06+01:00 Download 5ff4e3e
Download 9fa77c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-05T18:09:51+01:00 Download a2114c0
Download 6f16361 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2020-12-07T23:09:30+01:00
Download 003815b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 3 2020-12-09T22:05:32+01:00 Download 9afec46
Download 8ebee87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 3 2020-12-09T04:12:43+01:00 Download cedd224
Download a2114c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 3 2020-12-05T16:56:09+01:00
Download c1ebd0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0 3 2020-12-07T16:09:34+01:00 Download aad1f3b
Download d00502d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-09T01:49:10+01:00 Download 1c69ee9
Download 3fa71dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-08T06:36:42+01:00 Download 6f16361
Download bf5ecfb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-06T18:27:11+01:00 Download 5ff4e3e

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download bdc4770 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2019-12-01 20:50:57
Download ed0ee70 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:33:58+01:00 Download a794efc
Download 51168b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:09:38+01:00 Download bdc4770
Download 3a3e9f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-08T00:26:51+01:00 Download 2ffc23e
Download ce3ab92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-08T00:07:35+01:00 Download cb646d4
Download 343a744 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-06T02:39:28+01:00 Download 44f835f
Download 9a4ec8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-05T20:20:50+01:00 Download f5560b9
Download 3cf6eee Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-11-29T15:27:54+01:00
Download 24c741b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 3 2019-12-03T08:57:50+01:00 Download f2491f9
Download fc5d25d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 3 2019-12-03T08:31:21+01:00 Download 3cf6eee
Download a794efc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 3 2019-11-30T22:03:27+01:00
Download 1c2716f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:43:51+01:00 Download 1c475e3
Download 07145b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 3 2019-12-07T21:13:52+01:00 Download d6a5916
Download cd3ee52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.9 3 2019-12-11T20:54:30+01:00 Download 0493508

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7d33d13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T07:36 CET (sv-comp)
Download db297f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-10T10:48:39+01:00 Download 885fa78
Download 18f5ffd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:53:05+01:00 Download c4a8c93
Download ebc08d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:24:29+01:00 Download a73d04b
Download 1c28942 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T08:56:43+01:00 Download b0cd215
Download 1d25d48 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:18:18+01:00 Download 8f70620
Download b0cd215 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 3 2018-12-07T20:44:38+01:00
Download 57d9e57 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T22:07:27+01:00 Download 2e3bf58
Download e03b27f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-07T09:15:41+01:00 Download 156de7e
Download c012e29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:15:13+01:00 Download d2a3ae4
Download 959ad92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-05T18:26:12+01:00
Download fbe88e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-06T10:20:13+01:00 Download 6a618d5
Download 2e3bf58 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-08T02:06:38
Download b376c50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:37:43+01:00 Download 8a53cd6
Download c8c4a79 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T23:42:34+01:00 Download 7d33d13
Download b2977f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T03:24:54+01:00 Download 885fa78
Download b5c2250 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:48:10+01:00 Download 959ad92
Download f5f51ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-08T05:06:19+01:00 Download 434e02f

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 323a41e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-02T23:42 CET (sv-comp)
Download ac08659 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.6.1-svn 26773 3 2017-12-01T08:29:16+01:00
Download b3e2912 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T10:34:39.094221
Download 30f7702 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:36:24.177572
Download 9f129de 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 547f8f9 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:47Z
Download 2f64a07 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:14 CET (sv-comp)
Download 9d536e2 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:28 CET (sv-comp)
Download a4abc45 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-03T04:18Z
Download 156de7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2017-12-01T21:49 CET (sv-comp)
Download 2a99505 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Map2Check 2 2017-12-01T23:47 CET (sv-comp)

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

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

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

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