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/memset2_false-valid-deref-write.c
programSHA d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a
witnessName results-verified/predatorhp.2017-12-01_2145.logfiles/sv-comp18.memset2_false-valid-deref-write.c.files/witness.graphml
witnessSHA 63447bcd37b05c66d1d8b8a5d05235c3f7cb4752f8347d945cbe472f28c867f8

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/63447bcd37b05c66d1d8b8a5d05235c3f7cb4752f8347d945cbe472f28c867f8.json

Key Value
architecture 32bit
creationtime 2017-12-01T21:54 CET (sv-comp)
memorymodel precise
producer PredatorHP
program-sha256 d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a
programfile ../../sv-benchmarks/c/ldv-memsafety/memset2_false-valid-deref-write.c
programhash 504b8754db5656e557502f2f9e958956c9b0cd94
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-deref) )
witness-file witnessFileByHash/63447bcd37b05c66d1d8b8a5d05235c3f7cb4752f8347d945cbe472f28c867f8.graphml
witness-sha256 63447bcd37b05c66d1d8b8a5d05235c3f7cb4752f8347d945cbe472f28c867f8
witness-size 3774
witness-type violation_witness

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2adad80 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T08:05:22+01:00
Download 32a0543 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2023-11-29T23:51:36Z
Download 518d8bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-19T15:33:45+01:00 Download 3b1c05c
Download f0d618d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-19T05:28:09+01:00 Download 2a3ced6
Download 926bb1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-18T12:07:24+01:00 Download 2adad80
Download 0a981e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-18T03:09:33+01:00 Download 9791efd
Download 12aba3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-17T22:10:15+01:00 Download fc6ba23
Download 8ed26a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-05T14:39:22+01:00 Download 6cec610
Download cf004af Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-04T16:44:08+01:00 Download 10da975
Download ef552a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-04T02:25:21+01:00 Download 4eb3a2b
Download c8c0c9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-12-01T22:53:41+01:00 Download 91db460
Download 8153aa8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T13:43:16+01:00 Download f0da481
Download 455f3e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T09:44:07+01:00 Download 9b29e71
Download f0da481 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T06:22:29+01:00
Download 97984df Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-30T03:04:54+01:00 Download 32a0543
Download 94c9d9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.3 3 2023-11-28T23:50:05+01:00 Download 18005a7
Download 4eb3a2b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 3 2023-12-04T00:20:13+01:00
Download 3b1c05c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2023-12-19T11:59:51+01:00
Download 9791efd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 3 2023-12-18T01:56:42+01:00
Download bbea0b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-12-04T12:13:23+01:00 Download dd99a6d
Download da8f661 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-12-03T06:19:21+01:00 Download e88b063
Download 9115c02 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-12-01T18:29:02+01:00 Download 12977b1
Download bb0e6f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-11-29T08:33:44+01:00 Download 551ee3d
Download 12977b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.4.0 incr 4 2023-12-01T13:15:30Z
Download dd99a6d 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-02T19:09:33Z
Download e88b063 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:57:11Z
Download fc6ba23 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-17T09:42:45+01:00
Download 551ee3d 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-29T04:15:23Z
Download 18005a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness sv-sanitizers 0.1.1 3 2023-11-28T20:03:54Z
Download 9b29e71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2023-11-30T08:25:56Z
Download 2a3ced6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2023-12-18T17:06:20+01:00
Download 6cec610 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-05T11:42:41Z
Download 10da975 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-04T14:51:17Z
Download 91db460 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2023-12-01T21:10:57Z
Download 6fb3945 Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow location: column: 3 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4bd30fa3-bf96-429c-ade8-97ab67d53617/sv-benchmarks/c/ldv-memsafety/memset2_-write.c line: 22 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T23:51:36Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4bd30fa3-bf96-429c-ade8-97ab67d53617/sv-benchmarks/c/ldv-memsafety/memset2_-write.c : d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4bd30fa3-bf96-429c-ade8-97ab67d53617/sv-benchmarks/c/ldv-memsafety/memset2_-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:31+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download db289b6 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T06:23:55+01:00
Download 95390c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2022-12-12T14:15:20Z
Download ebd4a4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T05:58:20+01:00 Download 95390c7
Download edfbe7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T04:19:12+01:00 Download cc883df
Download 984f3e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T01:30:55+01:00 Download 2de03ab
Download 8cc1f6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-29T00:54:52+01:00 Download 487a05a
Download 45f64df Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T21:08:39+01:00 Download 7af74c3
Download d7f6e28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T14:17:24+01:00 Download db289b6
Download a52e615 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T08:55:23+01:00 Download 7a9ed6c
Download 7d8d126 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T06:00:58+01:00 Download c9aa084
Download 1e9dd6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T04:23:36+01:00 Download ead463b
Download 691ba6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2023-01-28T00:29:48+01:00 Download c812453
Download 7a9ed6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2 3 2022-12-10T19:50:40+01:00
Download 2de03ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 3 2022-12-12T02:21:26+01:00
Download 487a05a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2022-12-11T03:36:17+01:00
Download 7af74c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2022-12-10T03:12:52+01:00
Download c9aa084 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 3 2022-12-09T03:04:36+01:00
Download 9b6faed Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-29T10:43:27+01:00 Download 1f02553
Download 0d06511 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-29T06:54:50+01:00 Download 984a502
Download 15e86a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-29T06:38:33+01:00 Download d30cd71
Download 89eaf45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-28T15:45:34+01:00 Download ce2d7dd
Download 24d1248 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-28T02:23:37+01:00 Download c7bb2d8
Download ce2d7dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 7.0.0 incr 4 2022-12-18T16:10:54Z
Download c7bb2d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2022-12-25T08:21:26Z
Download 1f02553 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:57:49Z
Download d30cd71 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:45:39Z
Download ead463b 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-08T07:47:12+01:00
Download 984a502 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-13T18:17:40Z
Download c812453 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Bubaak 3 2022-12-08T14:25:55Z

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ffc22cf Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T09:13:40+01:00
Download fcf084c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2021-12-10T17:48:09
Download 76a34c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 3 2021-12-07T15:45:53Z
Download 2ca76d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-10T21:28:40+01:00 Download fcf084c
Download 2dfda2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-09T16:02:25+01:00 Download 76fd1c9
Download b55257d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-09T06:21:15+01:00 Download cc883df
Download c7a8028 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-08T21:09:28+01:00 Download a5cca86
Download f379be4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T19:12:51+01:00 Download 76a34c8
Download b01a28c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T11:25:54+01:00 Download ffc22cf
Download 7a502f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-07T04:56:02+01:00 Download b728354
Download 553bba2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-06T11:48:37+01:00 Download 52d9b18
Download 4ea3e4a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-05T20:39:59+01:00 Download 204bec0
Download 204bec0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.1 3 2021-12-05T18:06:13+01:00
Download 76fd1c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2021-12-09T12:06:02+01:00
Download b728354 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-38892M 3 2021-12-07T02:30:25+01:00
Download 250c94d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-10T17:26:52+01:00 Download 0ac3a12
Download 1e556a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-10T08:34:32+01:00 Download 1197af1
Download ecf26fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-08T13:49:45+01:00 Download 0b34164
Download 556b835 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-07T02:35:19+01:00 Download fe2aa22
Download 0b34164 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 6.8.0 incr 4 2021-12-08T07:48:38Z
Download a5cca86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 3 2021-12-08T18:22:26+01:00
Download 1197af1 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-10T04:25:07Z
Download 0ac3a12 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:48:03Z
Download 52d9b18 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-06T07:17:34+01:00
Download fe2aa22 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:29:51Z

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c842339 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T18:15:44+01:00
Download b1f7065 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-11T23:00:53
Download 57c0bab Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 2 2020-12-08T13:59:58
Download e03e784 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-12T01:29:49+01:00 Download b1f7065
Download 8898dc3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-09T21:53:42+01:00 Download cb7efb4
Download 14e817e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-09T21:31:52+01:00 Download b9f34db
Download 7c48fa4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-09T02:25:21+01:00 Download 28b84bc
Download b69a1a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-08T07:47:31+01:00 Download 1729b64
Download 7b97bd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-06T18:26:39+01:00 Download 6ce96e2
Download 1784e09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0 3 2020-12-05T12:55:42+01:00
Download 1729b64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2020-12-07T23:51:33+01:00
Download d1bf9b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 3 2020-12-07T16:31:09+01:00 Download b9fb5a9
Download 7bce899 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 3 2020-12-09T04:03:27+01:00 Download 57c0bab
Download 651a4a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 3 2020-12-06T19:41:05+01:00 Download c842339
Download 211893c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 2.0 3 2020-12-05T18:41:12+01:00 Download 1784e09
Download 6f0d8a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-06T18:02:15+01:00 Download 1784e09
Download 7bc8e82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 2.0 3 2020-12-06T07:50:44+01:00 Download 6ce96e2

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 07bb3d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2019-12-01 15:36:05
Download f682d5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:41:47+01:00 Download f9e9ca4
Download 66a38f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:09:20+01:00 Download 07bb3d2
Download 880b787 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-08T00:26:44+01:00 Download b7b57f2
Download 07fa934 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-08T00:07:38+01:00 Download cc883df
Download 201aea1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-06T02:40:21+01:00 Download c1a3f5a
Download 7da9acf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-12-05T20:20:13+01:00 Download 9eba3d4
Download 13767c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 3 2019-11-29T23:50:29+01:00
Download 3cd4bb5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 3 2019-12-11T20:54:52+01:00 Download 4a9e10f
Download 095f426 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 3 2019-12-07T21:16:52+01:00 Download 80f9c1b
Download b494405 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 3 2019-12-03T08:57:38+01:00 Download ddf80e2
Download 220cf4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.9 3 2019-12-03T08:10:13+01:00 Download 13767c5
Download 7a1c435 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.9 3 2019-12-11T21:46:22+01:00 Download f1355c5
Download f9e9ca4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 3 2019-12-01T00:25:40+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6033ad6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T13:16 CET (sv-comp)
Download 47400f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 3 2018-12-07T02:49:26+01:00
Download b10bbf9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:53:26+01:00 Download 0a34946
Download bae3769 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:33:41+01:00 Download 1e7c926
Download b87550e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T22:10:02+01:00 Download d627739
Download 9dba359 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T08:53:35+01:00 Download 47400f3
Download f6f770d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:48:12+01:00 Download 89c78e8
Download 1dd3a9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:17:20+01:00 Download dafc93b
Download a583b46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-06T10:19:22+01:00 Download 4cc052d
Download 6a281a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T23:44:04+01:00 Download 6033ad6
Download a59116a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-07T09:16:57+01:00 Download 63447bc
Download 8026d5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-08T05:05:13+01:00 Download d15dfdb
Download d627739 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-08T06:02:57
Download 5c6bcd7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-10T10:48:52+01:00 Download cf1f8fd
Download af4ab0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-09T20:18:11+01:00 Download 4e1e927
Download 9006d91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-08T03:33:10+01:00 Download cf1f8fd
Download 996b8a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:13:36+01:00 Download e6dbc0e
Download 89c78e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-05T22:30:32+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e3c6765 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-02T23:30 CET (sv-comp)
Download 506ebc9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.6.1-svn 26773 3 2017-12-01T08:34:13+01:00
Download 506f5b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T12:00:16.837611
Download dad43fd 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:41:20.690035
Download 9a70254 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 3 2017-12-03T06:53Z
Download 08d0097 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:57Z
Download 1f8fe1d 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:33 CET (sv-comp)
Download 3f338c5 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 17836dd 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:25Z
Download 63447bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness PredatorHP 4 2017-12-01T21:54 CET (sv-comp)
Download 5164507 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness Map2Check 2 2017-12-01T23:16 CET (sv-comp)

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

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

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

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