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 (ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8, sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c).

Found 58 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c, ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 9f4ff8c Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2023-12-18T09:33:22+01:00
Download e24e4b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2023-11-29T20:50:15Z
Download 60d39a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 7 2023-11-30T07:48:32+01:00
Download 965c09d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 7 2023-12-03T20:23:35+01:00
Download c78d9d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 7 2023-12-18T19:30:34+01:00
Download 60335cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 10 2023-12-18T02:00:13+01:00
Download cd89df5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-05T12:45:08Z
Download 4857cea Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-04T12:38:42Z
Download c407cb7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-01T20:34:13Z
Download c13e08a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 7.4.0 incr 3 2023-12-01T13:30:38Z
Download 317ba6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 13 2023-12-02T16:51:37Z
Download 956a958 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness PredatorHP 4 2023-11-30T08:24:28Z
Download 32267c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T16:38:00Z
Download 7742048 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CBMC 397 2023-12-17T11:15:15+01:00
Download f9c9f44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 12 2023-11-28T23:01:08Z
Download 20ede22 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-17T21:47:06+01:00 Download a549183
Download 57229ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 19 2023-11-29T08:23:03+01:00 Download ac24e22
Download afc642b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:51:02+01:00
Download 5bc4e21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2023-12-03T07:27:54Z
Download 4bfd27c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness crux-llvm-0.5.0.99 3 2023-12-18T05:12:07+01:00
Download 4e20cb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download 5ff6d49 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 13 2023-12-02T11:44:32Z
Download 62689a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2023-12-17T02:07:13Z
Download 8f1a732 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2023-11-29T20:36:14Z
Download 7510f24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2023-12-20T00:21:54
Download f47e740 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T13:59:27Z
Download 39b0e3a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 7.4.0 kind 3 2023-12-01T11:13:05Z
Download fabd0fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-12-20T02:16:39+01:00 Download 7510f24
Download c7c47ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-12-18T06:16:17+01:00 Download 4bfd27c
Download 4233d45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-12-17T06:11:32+01:00 Download 62689a0
Download 2f850e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-12-05T14:22:00+01:00 Download 3760978
Download b5f8ba0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-12-04T16:28:21+01:00 Download 966a539
Download 182e3ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 22 2023-12-04T11:59:43+01:00 Download 5ff6d49
Download 4a73b69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-12-03T18:33:13+01:00 Download afc642b
Download 5ff8fea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-12-03T09:54:23+01:00 Download 5bc4e21
Download 807ee59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-12-01T22:45:52+01:00 Download 3481e9b
Download 63bfeaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-12-01T17:59:51+01:00 Download 39b0e3a
Download 82ff1d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-11-30T07:01:09+01:00
Download f8cfdfc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-11-30T02:34:10+01:00 Download 8f1a732
Download 46ab9e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-11-29T18:30:22+01:00 Download f47e740
Download 523f82f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 9 2023-12-03T23:28:41+01:00
Download af7e981 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 9 2023-12-18T18:19:00+01:00
Download a549183 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 397 2023-12-17T17:23:52+01:00
Download 3760978 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-05T09:11:54Z
Download 966a539 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-04T12:29:08Z
Download 3481e9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-01T20:27:10Z
Download ac24e22 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 14 2023-11-29T01:24:13Z
Download efba52e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.4.0 3 2023-12-01T15:09:24Z
Download a680226 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2023-12-17T01:45:42Z
Download 8134ee8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2023-11-29T19:29:20Z
Download eda39cf Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2023-12-19T22:41:23
Download bc5bc23 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 397 2023-12-17T09:38:46+01:00
Download a093615 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-05T10:27:37Z
Download 7795cfb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-04T08:59:15Z
Download f2f8131 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-01T21:11:05Z
Download 0387cfb Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: d9b91130-78f1-485e-b510-68286835157d creation_time: '2023-11-29T02:24:13+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_53814947-e697-44db-8282-28ada0c2dbea/sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_53814947-e697-44db-8282-28ada0c2dbea/sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration.c : ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 32bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_53814947-e697-44db-8282-28ada0c2dbea/sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration.c file_hash: ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8 line: 26 column: 0 function: main value: ((i == 0) || ((1 <= i) && (i <= 2147483645))) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_53814947-e697-44db-8282-28ada0c2dbea/sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration.c file_hash: ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8 line: 29 column: 0 function: main value: ((i == 0) || ((i <= 2147483646) && (1 <= i))) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_53814947-e697-44db-8282-28ada0c2dbea/sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration.c file_hash: ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8 line: 17 column: 0 function: foo value: (((((((i <= 2147483644) && (i == 0)) && (1 <= size)) && (i == size)) || (((i == 0) && (size == 0)) && (i == 0))) || (((i == 0) && (size == 0)) && (i == 1))) || ((((i <= 2147483644) && (1 <= i)) && (1 <= i)) && (i == size))) format: c_expression correctness_witness CPAchecker 2.3 11 2023-11-29T07:47:54+01:00
Download 86a9fb9 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 1433a518-ec84-401a-bb33-dea5810d24d0 creation_time: '2023-12-02T12:44:32+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5039d370-8077-4de1-9265-adf3ba85dc58/sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5039d370-8077-4de1-9265-adf3ba85dc58/sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration.c : ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 32bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5039d370-8077-4de1-9265-adf3ba85dc58/sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration.c file_hash: ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8 line: 29 column: 0 function: main value: ((i == 0) || ((i <= 2147483646) && (1 <= i))) format: c_expression correctness_witness CPAchecker 2.3 10 2023-12-04T11:57:26+01:00
Download afc0882 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: d9438d38-1633-4f1f-826a-d136d27a8763 creation_time: 2023-12-01T01:50:38Z producer: name: Goblint version: tags/svcomp24-0-gc2e9465a7 command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--sets'' ''ana.specification'' ''../../sv-benchmarks/c/properties/no-overflow.prp'' ''--sets'' ''exp.architecture'' ''32bit'' ''../../sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration.c''' task: input_files: - ../../sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration.c input_file_hashes: ../../sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration.c: ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8 data_model: ILP32 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration.c file_hash: ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8 line: 17 column: 8 function: foo value: ((((size != 0 && ((((((((((((((((((((((12 <= i && ((((12 <= size && (-24LL + (long long )i) + (long long )size >= 0LL) && (0LL - (long long )i) + (long long )size >= 0LL) && i != 0) || ((11 <= size && (-23LL + (long long )i) + (long long )size >= 0LL) && (1LL - (long long )i) + (long long )size >= 0LL))) || (((11 <= size && (-22LL + (long long )i) + (long long )size >= 0LL) && (0LL - (long long )i) + (long long )size >= 0LL) && i == 11)) || (((10 <= size && (-21LL + (long long )i) + (long long )size >= 0LL) && (1LL - (long long )i) + (long long )size >= 0LL) && i == 11)) || (((10 <= size && (-20LL + (long long )i) + (long long )size >= 0LL) && (0LL - (long long )i) + (long long )size >= 0LL) && i == 10)) || (((9 <= size && (-19LL + (long long )i) + (long long )size >= 0LL) && (1LL - (long long )i) + (long long )size >= 0LL) && i == 10)) || (((9 <= size && (-18LL + (long long )i) + (long long )size >= 0LL) && (0LL - (long long )i) + (long long )size >= 0LL) && i == 9)) || (((8 <= size && (-17LL + (long long )i) + (long long )size >= 0LL) && (1LL - (long long )i) + (long long )size >= 0LL) && i == 9)) || (((8 <= size && (-16LL + (long long )i) + (long long )size >= 0LL) && (0LL - (long long )i) + (long long )size >= 0LL) && i == 8)) || (((7 <= size && (-15LL + (long long )i) + (long long )size >= 0LL) && (1LL - (long long )i) + (long long )size >= 0LL) && i == 8)) || (((7 <= size && (-14LL + (long long )i) + (long long )size >= 0LL) && (0LL - (long long )i) + (long long )size >= 0LL) && i == 7)) || (((6 <= size && (-13LL + (long long )i) + (long long )size >= 0LL) && (1LL - (long long )i) + (long long )size >= 0LL) && i == 7)) || (((6 <= size && (-12LL + (long long )i) + (long long )size >= 0LL) && (0LL - (long long )i) + (long long )size >= 0LL) && i == 6)) || (((5 <= size && (-11LL + (long long )i) + (long long )size >= 0LL) && (1LL - (long long )i) + (long long )size >= 0LL) && i == 6)) || (((5 <= size && (-10LL + (long long )i) + (long long )size >= 0LL) && (0LL - (long long )i) + (long long )size >= 0LL) && i == 5)) || (((4 <= size && (-9LL + (long long )i) + (long long )size >= 0LL) && (1LL - (long long )i) + (long long )size >= 0LL) && i == 5)) || (((4 <= size && (-8LL + (long long )i) + (long long )size >= 0LL) && (0LL - (long long )i) + (long long )size >= 0LL) && i == 4)) || (((3 <= size && (-7LL + (long long )i) + (long long )size >= 0LL) && (1LL - (long long )i) + (long long )size >= 0LL) && i == 4)) || (((3 <= size && (-6LL + (long long )i) + (long long )size >= 0LL) && (0LL - (long long )i) + (long long )size >= 0LL) && i == 3)) || (((2 <= size && (-5LL + (long long )i) + (long long )size >= 0LL) && (1LL - (long long )i) + (long long )size >= 0LL) && i == 3)) || (((2 <= size && (-4LL + (long long )i) + (long long )size >= 0LL) && (0LL - (long long )i) + (long long )size >= 0LL) && i == 2)) || (((1 <= size && (-3LL + (long long )i) + (long long )size >= 0LL) && (1LL - (long long )i) + (long long )size >= 0LL) && i == 2)) || (((1 <= size && (-2LL + (long long )i) + (long long )size >= 0LL) && (0LL - (long long )i) + (long long )size >= 0LL) && i == 1))) || (((0 <= size && (-1LL + (long long )i) + (long long )size >= 0LL) && (1LL - (long long )i) + (long long )size >= 0LL) && i == 1)) || (((0 <= size && (0LL - (long long )i) + (long long )size >= 0LL) && (long long )i + (long long )size >= 0LL) && i == 0)) || (((0 <= size && (0LL - (long long )i) + (long long )size >= 0LL) && (long long )i + (long long )size >= 0LL) && i == 0)) || ((0 <= size && (2147483648LL + (long long )i) + (long long )size >= 0LL) && (2147483647LL - (long long )i) + (long long )size >= 0LL) format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration.c file_hash: ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8 line: 29 column: 5 function: main value: (((((((((((((((((((((((((((((((((((((((((((((((((((i == 7 || i == 21) || i == 6) || i == 20) || i == 6) || i == 20) || i == 5) || i == 19) || i == 5) || i == 19) || i == 4) || i == 18) || i == 4) || i == 18) || i == 3) || i == 17) || i == 3) || i == 17) || i == 2) || i == 16) || i == 2) || i == 16) || i == 1) || i == 15) || i == 1) || i == 15) || (0 == i && i == 0)) || i == 14) || (0 == i && i == 0)) || i == 14) || 8 <= i) || i == 13) || i == 13) || i == 12) || i == 12) || i == 11) || (25 <= i && i != 0)) || i == 11) || (25 <= i && i != 1)) || i == 10) || i == 24) || i == 10) || i == 24) || i == 9) || i == 23) || i == 9) || i == 23) || i == 8) || i == 22) || i == 8) || i == 22) || i == 7) || i == 21 format: c_expression correctness_witness CPAchecker 2.3 16 2023-12-01T04:57:40+01:00

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

Trying to find witnesses for program (ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8, sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c).

Found 48 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c, ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 93f2bda Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2022-12-09T06:37:21+01:00
Download 558aa80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 7 2022-12-10T14:49:18+01:00
Download ff2eacd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 7 2022-12-11T21:51:51+01:00
Download 89ca421 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 7 2022-12-09T16:55:33+01:00
Download 7cbbfaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 10 2022-12-09T02:14:44+01:00
Download 0239f6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2022-12-08T20:05:33Z
Download 1ebee54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 7.0.0 incr 3 2022-12-18T17:25:18Z
Download e20662d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 6.8.0 incr 3 2022-12-25T10:16:17Z
Download 716b67a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 12 2022-12-14T07:07:42Z
Download fea5ab9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T09:03:11Z
Download bc0f95d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CBMC 397 2022-12-08T07:57:36+01:00
Download 1f772ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 12 2022-12-13T19:38:33Z
Download 89dfe42 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 14 2023-01-29T07:20:14+01:00 Download bf3737d
Download 72a9e62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-29T02:48:28+01:00 Download 0993619
Download c7ca8c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-28T11:20:33+01:00 Download 1644a5d
Download ad3c2d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-28T03:57:29+01:00 Download 41fee68
Download 509c7e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-11T01:44:08+01:00
Download 07a5282 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2022-12-09T11:36:37Z
Download 2d524c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness crux-llvm-0.5.0.99 3 2022-12-09T03:43:01+01:00
Download 4e20cb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T11:01 CET (comp)
Download ee01200 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 13 2022-12-14T03:42:30Z
Download 73530c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2022-12-25T11:58:00Z
Download dd7b494 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2022-12-12T10:02:29Z
Download eb23f03 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2022-12-11T18:08:29
Download d69c147 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T12:02:38Z
Download daa6ff4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 7.0.0 kind 3 2022-12-18T23:55:37Z
Download 95adfe5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-29T10:51:35+01:00 Download ee01200
Download 4611f3b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-29T05:25:34+01:00 Download dd7b494
Download 3c2898a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-29T04:50:55+01:00 Download eb23f03
Download 9e2d0eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-28T22:51:43+01:00 Download 509c7e3
Download 0dee8c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-28T17:38:44+01:00 Download 07a5282
Download 5132ee7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-28T15:02:04+01:00 Download daa6ff4
Download 0776d6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-28T08:20:23+01:00 Download 2d524c1
Download 540c2e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-28T01:04:35+01:00 Download 73530c3
Download 6974818 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-27T23:43:13+01:00 Download ccf5701
Download 1644a5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2022-12-10T16:40:18+01:00
Download 0993619 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 9 2022-12-11T20:52:19+01:00
Download edfe8b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 9 2022-12-10T00:12:27+01:00
Download 41fee68 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 397 2022-12-08T09:15:29+01:00
Download ccf5701 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2022-12-08T14:58:31Z
Download bf3737d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 13 2022-12-13T13:20:57Z
Download 15f3861 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2022-12-25T11:22:23Z
Download 50c4c21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.0.0 3 2022-12-19T02:21:45Z
Download 1ced7df Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2022-12-25T11:22:23Z
Download 4646213 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2022-12-12T15:52:18Z
Download ef682d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2022-12-11T15:05:45
Download 65e5c5a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 397 2022-12-08T12:55:58+01:00
Download c99126d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2022-12-08T20:12:01Z

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

Trying to find witnesses for program (ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8, sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c).

Found 15 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c, ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8d5a904 Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2021-12-07T08:02:50+01:00
Download 5d89575 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 7 2021-12-05T17:54:04+01:00
Download 334e893 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 7 2021-12-09T12:48:08+01:00
Download b7ff94c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 10 2021-12-07T02:40:24+01:00
Download 115901c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 6.8.0 incr 3 2021-12-08T04:16:25Z
Download dbbd75b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 7 2021-12-08T18:35:42+01:00
Download 5a4a69a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 12 2021-12-10T06:25:02Z
Download 99edaeb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CBMC 397 2021-12-06T08:51:23+01:00
Download 13c0bc3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 12 2021-12-06T21:47:15Z
Download cdc2194 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness SESL 2 2021-12-06T11:20:18+01:00
Download 1666169 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2021-12-08T11:41:32Z
Download 6c36ed3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness VERIFUZZ 3 2021-12-11T09:33:57Z
Download b28f70c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2021-12-07T12:23:44Z
Download d855b29 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2021-12-09T05:10:11
Download dd98e58 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 397 2021-12-06T01:57:19+01:00

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

Trying to find witnesses for program (ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8, sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c).

Found 6 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c, ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b393535 Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2020-12-06T12:35:56+01:00
Download 0a84241 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 7 2020-12-08T05:56:04+01:00
Download 173279a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0 7 2020-12-05T15:56:16+01:00
Download 5b391f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T16:59:41
Download 1bc20be Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-08T19:06:52
Download d1605ea Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2020-12-08T10:52:49

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

Trying to find witnesses for program (ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8, sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c).

Found 3 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c, ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 965a00d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 7 2019-11-29T22:58:11+01:00
Download 060607a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 7 2019-12-01T00:43:56+01:00
Download 1c46e41 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:11 CET (comp)

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

Trying to find witnesses for program (ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8, sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c).

Found 5 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c, ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7a56d28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2018-12-08T12:42 CET (sv-comp)
Download 970c915 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-05T20:00:35+01:00
Download ca4fd16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 8 2018-12-07T06:51:32+01:00
Download 7f7be8a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T07:40 CET (sv-comp)
Download 5db5755 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T09:21 CET (sv-comp)

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

Trying to find witnesses for program (ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8, sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c).

Found 15 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c, ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 16d601e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2017-12-03T00:29 CET (sv-comp)
Download 3090ce6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T08:25:00+01:00
Download 4646fc0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T11:22:09.851676
Download 670f27b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T23:46:42.742460
Download 684e643 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.6.1-svn 8 2017-12-01T09:49:42+01:00
Download 4aecc28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 9 2017-12-03T06:53Z
Download f0633b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Map2Check 4 2017-12-01T23:51 CET (sv-comp)
Download 1911404 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CBMC 485 2017-12-01T08:19 CET (sv-comp)
Download 94cfb3b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 9 2017-12-03T04:06Z
Download 575f875 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness 2LS 17 2017-12-01T08:19 CET (sv-comp)
Download c5e41d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 140 2017-12-01T19:36 CET (sv-comp)
Download 8e0fbe5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T21:17:21.024488
Download acba61f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T10:24:16.900446
Download 9419c3c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 470 2017-12-01T16:00 CET (sv-comp)
Download 714c2e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 16 2017-12-01T13:23 CET (sv-comp)

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

Trying to find witnesses for program (ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8, sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c, ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ef4a52e45666a829b602608a46cff9c8137910dd58bdfaebe016ce17984d1ac8.json

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