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/memsetNonZero3_false-valid-deref-write.c
programSHA f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7
witnessName results-validated/cpa-seq-validate-violation-witnesses-depthk.2018-12-06_1002.logfiles/sv-comp19_prop-memsafety.memsetNonZero3_false-valid-deref-write.c.files/witness.graphml
witnessSHA 6e864d9a32690a9f4627cad84f8412230b8de46c770c89dd8d6677f52f2bea96

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T10:18:29+01:00
inputwitnesshash ad826b5fcce1805464a03f0d4208c61885df3a46daa7a2c36f66ac3d9f960914
producer CPAchecker 1.7-svn 29852
program-sha256 f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7
programfile ../../sv-benchmarks/c/ldv-memsafety/memsetNonZero3_false-valid-deref-write.c
programhash f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-deref) )
witness-file witnessFileByHash/6e864d9a32690a9f4627cad84f8412230b8de46c770c89dd8d6677f52f2bea96.graphml
witness-sha256 6e864d9a32690a9f4627cad84f8412230b8de46c770c89dd8d6677f52f2bea96
witness-size 3048
witness-type correctness_witness

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2b09132 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T10:41:49+01:00
Download 375ec18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2023-12-17T04:34:24Z
Download aef3724 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2023-11-29T18:53:52Z
Download 0e97b55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-19T15:34:17+01:00 Download d40652f
Download 9c31ac5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-19T05:26:53+01:00 Download b7ec33a
Download 69448ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-18T12:01:41+01:00 Download 2b09132
Download a54d9ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-18T03:09:40+01:00 Download 8dd3217
Download 25c9846 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-17T22:06:54+01:00 Download 5475db1
Download 0f8b7d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-17T06:39:15+01:00 Download 375ec18
Download 2ad582e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-05T14:40:24+01:00 Download c498fc2
Download 1b07e6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-04T16:39:23+01:00 Download c562717
Download 737235d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-04T02:27:21+01:00 Download a0166eb
Download 7410644 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-01T22:56:27+01:00 Download de7cef9
Download 040ea29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T13:43:05+01:00 Download 5f89981
Download 81d606b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T09:44:13+01:00 Download d10b9d5
Download 000fe8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T03:05:30+01:00 Download aef3724
Download 5f89981 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T02:09:53+01:00
Download 1f39e26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-28T23:50:01+01:00 Download 546bc2b
Download a0166eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 3 2023-12-03T23:34:06+01:00
Download 8dd3217 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 4 2023-12-18T01:36:11+01:00
Download e88e438 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-12-04T12:12:12+01:00 Download 32c437d
Download 0b54f46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-12-03T06:19:15+01:00 Download a9dd65d
Download 986ece0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-12-01T18:29:54+01:00 Download a839416
Download 21985b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-11-29T08:33:38+01:00 Download defe1be
Download a839416 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:05:01Z
Download d40652f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 3 2023-12-19T11:43:25+01:00
Download 32c437d 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-02T17:28:46Z
Download a9dd65d 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:23:13Z
Download 5475db1 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-17T05:53:59+01:00
Download defe1be 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:07:14Z
Download 546bc2b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness sv-sanitizers 0.1.1 3 2023-11-28T22:18:21Z
Download d10b9d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2023-11-30T08:23:47Z
Download b7ec33a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2023-12-18T20:15:33+01:00
Download c498fc2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-05T12:54:41Z
Download c562717 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-04T08:51:28Z
Download de7cef9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-01T20:30:10Z
Download db85ef5 Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow location: column: 3 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_82768315-0a4e-4798-95c3-ae37d9c7b66e/sv-benchmarks/c/ldv-memsafety/memsetNonZero3_-write.c line: 29 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T18:53:52Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_82768315-0a4e-4798-95c3-ae37d9c7b66e/sv-benchmarks/c/ldv-memsafety/memsetNonZero3_-write.c : f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_82768315-0a4e-4798-95c3-ae37d9c7b66e/sv-benchmarks/c/ldv-memsafety/memsetNonZero3_-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:59:45+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7a427d3 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T06:56:02+01:00
Download e7a3243 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-25T11:59:24Z
Download de49dfd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-12T11:42:19Z
Download 174e7fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T05:58:18+01:00 Download de49dfd
Download 2ea73cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T04:19:13+01:00 Download c054602
Download a6f6e2e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T01:30:42+01:00 Download f908cf0
Download 88a6eb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T00:54:14+01:00 Download ab50d61
Download 3237782 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T21:08:40+01:00 Download 8790126
Download 4015550 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T14:19:19+01:00 Download 7a427d3
Download 018a2dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T08:55:45+01:00 Download 2f358e4
Download 7f9755e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T06:01:06+01:00 Download 65aaa38
Download 2165e3e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T04:21:41+01:00 Download bcc8e02
Download 9026789 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T02:23:37+01:00 Download e7a3243
Download 4f5cf11 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T00:28:17+01:00 Download fe7aa15
Download 2f358e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2022-12-10T16:12:40+01:00
Download f908cf0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 3 2022-12-11T20:23:55+01:00
Download ab50d61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2022-12-11T06:01:59+01:00
Download 8790126 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2022-12-10T00:10:20+01:00
Download 65aaa38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 4 2022-12-09T03:06:20+01:00
Download 901f4dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-29T10:43:55+01:00 Download fa575b9
Download fe6f59c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-29T06:53:08+01:00 Download e8ff809
Download 00299c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-29T06:38:39+01:00 Download f99523b
Download 183f8a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-28T15:45:36+01:00 Download 74b1527
Download 74b1527 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.0.0 incr 4 2022-12-19T00:58:38Z
Download fa575b9 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:41Z
Download f99523b 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-14T20:33:08Z
Download bcc8e02 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-08T12:34:03+01:00
Download e8ff809 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-13T11:50:19Z
Download fe7aa15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2022-12-08T14:42:28Z

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 338012a Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T09:27:53+01:00
Download de3e03c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2021-12-10T17:02:22
Download e7416e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2021-12-07T15:19:14Z
Download 3a1adca Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-10T21:27:22+01:00 Download de3e03c
Download 1057ca0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-09T16:00:36+01:00 Download 21ea646
Download fae2957 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-09T06:22:08+01:00 Download c054602
Download ae480f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-08T21:11:10+01:00 Download 55957e1
Download 31da26c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T19:10:53+01:00 Download e7416e8
Download 7dce3e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T11:28:03+01:00 Download 338012a
Download 6eeb783 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T04:56:28+01:00 Download 6549ffa
Download f1e6aa8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-06T11:47:32+01:00 Download e61656a
Download 39c7d64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-05T20:38:29+01:00 Download 7831419
Download 7831419 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-05T17:07:29+01:00
Download 21ea646 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2021-12-09T14:35:35+01:00
Download 6549ffa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 4 2021-12-07T02:11:58+01:00
Download 5dcc32e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-10T17:27:45+01:00 Download c96ad26
Download 07571a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-10T08:34:07+01:00 Download 49e95aa
Download a308e02 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-08T13:50:21+01:00 Download 8061e9b
Download c0a34b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-07T02:35:09+01:00 Download 4033092
Download 8061e9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2021-12-08T10:32:20Z
Download 49e95aa 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:58:19Z
Download c96ad26 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:18:28Z
Download e61656a 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-06T04:13:50+01:00
Download 4033092 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-06T16:35:36Z
Download 55957e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 3 2021-12-08T19:37:48+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 66a9411 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T17:46:22+01:00
Download 22be08c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-11T22:19:01
Download 9b2f9aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-09T01:12:02
Download 6551674 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-12T01:30:23+01:00 Download 22be08c
Download f744a8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-08T06:46:11+01:00 Download fcecbf9
Download 6411dd1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-06T18:01:19+01:00 Download 7f4c537
Download 66326fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-05T18:36:59+01:00 Download 7f4c537
Download 7f4c537 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-05T15:23:32+01:00
Download 93836b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 3 2020-12-09T04:11:29+01:00 Download 9b2f9aa
Download 7809b7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 3 2020-12-09T02:37:56+01:00 Download fb61bc0
Download cf080bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 3 2020-12-06T18:26:42+01:00 Download d028d76
Download 07726a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0 3 2020-12-07T16:12:35+01:00 Download 90f42f9
Download 78aef1d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-09T21:56:09+01:00 Download 871826c
Download b847167 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-09T21:15:17+01:00 Download cbf8d32
Download b805905 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-06T19:05:38+01:00 Download 66a9411
Download 672c1c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-06T07:41:58+01:00 Download d028d76
Download fcecbf9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2020-12-08T00:05:02+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 9772ba7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2019-12-01 06:14:22
Download cde9c1a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:09:27+01:00 Download 9772ba7
Download 3b5026c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-08T00:26:19+01:00 Download b014204
Download 7d60072 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-06T02:40:29+01:00 Download 1956ecf
Download 4b818fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-05T20:20:23+01:00 Download 4ba71d0
Download 6d2e55d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-03T08:09:50+01:00 Download a5bfabc
Download 5988bb9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 3 2019-12-01T11:49:44+01:00
Download d5026c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 3 2019-12-11T20:54:52+01:00 Download faaf945
Download ba8d240 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:40:21+01:00 Download 0f2d847
Download d20d76f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 3 2019-12-08T00:06:01+01:00 Download c054602
Download 72fbe77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 3 2019-12-07T21:17:59+01:00 Download 4c132ac
Download bd5f812 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:39:48+01:00 Download 5988bb9
Download 6f3a00d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 3 2019-12-03T08:57:28+01:00 Download 7c37a5b
Download a5bfabc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 3 2019-11-29T23:33:17+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0192518 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T19:17 CET (sv-comp)
Download 8b59fc6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 3 2018-12-07T17:57:15+01:00
Download 894e9eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-10T10:48:43+01:00 Download 001761f
Download 9151aed Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:53:08+01:00 Download a5f95aa
Download dd74d0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T23:44:00+01:00 Download 0192518
Download 8e2eaed Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T22:10:05+01:00 Download 517c06e
Download c5c0528 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:01:14+01:00 Download a8b2a4f
Download 2fe8b1a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-05T09:33:22+01:00
Download 25ef98b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:34:10+01:00 Download 6b52329
Download 486e61d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T08:33:35+01:00 Download 8b59fc6
Download dc10f54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-07T09:26:48+01:00 Download 34592e2
Download c8781ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:07:22+01:00 Download 519bffe
Download 517c06e 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:18:05
Download 93d7fef Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:38:03+01:00 Download 24c20d4
Download 8a24673 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T04:25:09+01:00 Download 001761f
Download f23b301 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:49:09+01:00 Download 2fe8b1a
Download 86103e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-08T05:06:29+01:00 Download f1188dc
Download 6e864d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-06T10:18:29+01:00 Download ad826b5

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e240167 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-03T00:25 CET (sv-comp)
Download 7de639d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.6.1-svn 26773 3 2017-12-01T08:30:35+01:00
Download 15c8694 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:06.584146
Download f83cf46 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:52:25.095591
Download d607cf7 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:53Z
Download c558e6d 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:58Z
Download bec4fe4 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:19 CET (sv-comp)
Download 17a1954 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:27Z
Download 34592e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2017-12-01T22:01 CET (sv-comp)
Download 298359f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Map2Check 3 2017-12-01T23:16 CET (sv-comp)

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

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

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

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