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).
Found 37 witnesses for program sv-benchmarks/c/termination-memory-alloca/c.03-alloca_true-termination_true-no-overflow.c.i, ffd6e9554cad43049f3baa89c0ba2bf94011d3e069a47b1754df8be10679286a
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ffd6e9554cad43049f3baa89c0ba2bf94011d3e069a47b1754df8be10679286a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
27a92bb | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T08:59:06+01:00 | ||
5eb5c26 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T21:39:48Z | ||
6c56e7f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-18T12:04:01+01:00 | 27a92bb | |
06bc610 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T08:30:38+01:00 | ||
0059b69 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 6 | 2023-12-03T21:21:56+01:00 | ||
57fa388 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2023-12-18T19:27:59+01:00 | ||
cbf765e | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Taipan | 21 | 2023-12-02T12:21:24Z | ||
fb52029 | Inspect | 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:26:20Z | ||
93eb607 | Inspect | 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-29T11:21:51Z | ||
3cc8aac | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Kojak | 21 | 2023-12-02T20:32:16Z | ||
6d727e2 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 31 | 2023-12-01T01:51:36Z | ||
bd2cc08 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Automizer | 21 | 2023-11-29T03:02:49Z | ||
f858485 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:51:22+01:00 | ||
55d599a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T06:04:58Z | ||
de59e93 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 18 | 2023-12-02T18:45:52Z | ||
97f0f77 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2023-11-29T13:46:41Z | ||
53bbd03 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 18 | 2023-12-02T23:35:02Z | ||
c08b023 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-19T15:15:28+01:00 | b365ef6 | |
6b45f7f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-19T04:35:33+01:00 | 83fbac9 | |
4b00de4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-17T06:19:12+01:00 | 705d245 | |
87dddc3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-04T11:44:11+01:00 | de59e93 | |
147d81f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-04T02:05:26+01:00 | 5d3a4c8 | |
d5d0f63 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T18:36:27+01:00 | f858485 | |
83101fa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T09:54:05+01:00 | 55d599a | |
e119e84 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T06:00:52+01:00 | 53bbd03 | |
ecd9960 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T12:57:48+01:00 | f1179d6 | |
f1179d6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T06:07:19+01:00 | ||
268578d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-29T18:34:51+01:00 | 97f0f77 | |
24b0dae | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-29T08:24:20+01:00 | b5e0ef9 | |
5d3a4c8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 6 | 2023-12-03T23:14:57+01:00 | ||
705d245 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 6 | 2023-12-17T04:32:38+01:00 | ||
83fbac9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2023-12-18T18:36:52+01:00 | ||
b5e0ef9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 17 | 2023-11-29T01:08:32Z | ||
9d8b45c | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: e445bee9-fb5b-4378-9b1d-8ebc9b6be6b7 creation_time: '2023-12-03T00:35:02+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_bfe04b6a-8d78-46b7-9041-e2c95a76660a/sv-benchmarks/c/termination-memory-alloca/c.03-alloca-1.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_bfe04b6a-8d78-46b7-9041-e2c95a76660a/sv-benchmarks/c/termination-memory-alloca/c.03-alloca-1.i : ffd6e9554cad43049f3baa89c0ba2bf94011d3e069a47b1754df8be10679286a specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-03T05:44:03+01:00 | ||
c4eb90b | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 7ecdd67d-f2ea-4eda-8f6b-572b879345b8 creation_time: '2023-12-02T19:45:52+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ee7afe6d-95b4-4d61-8381-07d4d5006be2/sv-benchmarks/c/termination-memory-alloca/c.03-alloca-1.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ee7afe6d-95b4-4d61-8381-07d4d5006be2/sv-benchmarks/c/termination-memory-alloca/c.03-alloca-1.i : ffd6e9554cad43049f3baa89c0ba2bf94011d3e069a47b1754df8be10679286a specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-04T12:02:57+01:00 | ||
4eb3cce | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 50f6789d-6f1f-4c4c-9b60-9830c4b002a3 creation_time: '2023-11-29T02:08:32+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_1ee9fd12-d75b-4b07-a412-85a2b05c8f10/sv-benchmarks/c/termination-memory-alloca/c.03-alloca-1.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_1ee9fd12-d75b-4b07-a412-85a2b05c8f10/sv-benchmarks/c/termination-memory-alloca/c.03-alloca-1.i : ffd6e9554cad43049f3baa89c0ba2bf94011d3e069a47b1754df8be10679286a specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-29T07:46:26+01:00 | ||
8dfa2fd | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 0b095908-229c-4220-9913-8994304ddaa4 creation_time: 2023-12-01T01:00:36Z 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'' ''64bit'' ''../../sv-benchmarks/c/termination-memory-alloca/c.03-alloca-1.i''' task: input_files: - ../../sv-benchmarks/c/termination-memory-alloca/c.03-alloca-1.i input_file_hashes: ../../sv-benchmarks/c/termination-memory-alloca/c.03-alloca-1.i: ffd6e9554cad43049f3baa89c0ba2bf94011d3e069a47b1754df8be10679286a data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: [] | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-01T05:31:25+01:00 |
Found 28 witnesses for program sv-benchmarks/c/termination-memory-alloca/c.03-alloca_true-termination_true-no-overflow.c.i, ffd6e9554cad43049f3baa89c0ba2bf94011d3e069a47b1754df8be10679286a
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ffd6e9554cad43049f3baa89c0ba2bf94011d3e069a47b1754df8be10679286a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
38f183a | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:24:02+01:00 | ||
a957786 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T14:14:05+01:00 | 38f183a | |
e5356b3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 6 | 2022-12-10T14:47:13+01:00 | ||
4c9b89f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 6 | 2022-12-12T02:11:07+01:00 | ||
d3c6faa | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2022-12-10T00:54:15+01:00 | ||
c02a152 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Taipan | 20 | 2022-12-14T13:58:30Z | ||
bbb88f9 | Inspect | 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-11T12:20:59Z | ||
ceb924f | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Kojak | 20 | 2022-12-15T02:18:58Z | ||
91dee91 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Automizer | 20 | 2022-12-13T15:41:59Z | ||
855f0e6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-11T01:54:10+01:00 | ||
8a9aed5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T11:40:02Z | ||
a30db66 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 17 | 2022-12-14T07:56:14Z | ||
e2ce11a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2022-12-11T11:41:37Z | ||
39deb10 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 17 | 2022-12-15T00:40:00Z | ||
54d64a1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T11:08:01+01:00 | a30db66 | |
3eaef6a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T06:23:10+01:00 | 39deb10 | |
d3531aa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T03:45:45+01:00 | e2ce11a | |
afdb90d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T02:50:12+01:00 | 1a8a614 | |
92593ef | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T00:06:24+01:00 | 72e81e0 | |
63cf115 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T22:52:15+01:00 | 855f0e6 | |
58b8bd8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T18:44:56+01:00 | d253c34 | |
290cd4c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T17:38:30+01:00 | 8a9aed5 | |
226c0d4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T10:53:12+01:00 | 8bcfd2e | |
931291d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T00:46:21+01:00 | 980116a | |
8bcfd2e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2022-12-10T14:54:26+01:00 | ||
1a8a614 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 6 | 2022-12-12T02:39:57+01:00 | ||
980116a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 6 | 2022-12-25T09:26:18+01:00 | ||
d253c34 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2022-12-10T02:12:57+01:00 |
Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/c.03-alloca_true-termination_true-no-overflow.c.i, ffd6e9554cad43049f3baa89c0ba2bf94011d3e069a47b1754df8be10679286a
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ffd6e9554cad43049f3baa89c0ba2bf94011d3e069a47b1754df8be10679286a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
0750a6f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T16:20:59 |
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/c.03-alloca_true-termination_true-no-overflow.c.i, ffd6e9554cad43049f3baa89c0ba2bf94011d3e069a47b1754df8be10679286a
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ffd6e9554cad43049f3baa89c0ba2bf94011d3e069a47b1754df8be10679286a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c2daa6c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T21:27:45 | ||
519acc9 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-09T00:39:57 |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/c.03-alloca_true-termination_true-no-overflow.c.i, ffd6e9554cad43049f3baa89c0ba2bf94011d3e069a47b1754df8be10679286a
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ffd6e9554cad43049f3baa89c0ba2bf94011d3e069a47b1754df8be10679286a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/c.03-alloca_true-termination_true-no-overflow.c.i, ffd6e9554cad43049f3baa89c0ba2bf94011d3e069a47b1754df8be10679286a
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ffd6e9554cad43049f3baa89c0ba2bf94011d3e069a47b1754df8be10679286a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/c.03-alloca_true-termination_true-no-overflow.c.i, ffd6e9554cad43049f3baa89c0ba2bf94011d3e069a47b1754df8be10679286a
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ffd6e9554cad43049f3baa89c0ba2bf94011d3e069a47b1754df8be10679286a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
00b8fd2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 7 | 2017-12-01T17:42 CET (sv-comp) | ||
4eb2033 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 39 | 2017-12-01T11:49 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/c.03-alloca_true-termination_true-no-overflow.c.i, ffd6e9554cad43049f3baa89c0ba2bf94011d3e069a47b1754df8be10679286a
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ffd6e9554cad43049f3baa89c0ba2bf94011d3e069a47b1754df8be10679286a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |