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 36 witnesses for program sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i, ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8f35d16 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T09:18:09+01:00 | ||
90e6360 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-18T12:05:03+01:00 | 8f35d16 | |
692648f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T08:14:47+01:00 | ||
ce6b67d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 6 | 2023-12-03T23:35:22+01:00 | ||
364734c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2023-12-18T18:23:14+01:00 | ||
972e1dd | 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 | 10 | 2023-12-02T12:07:32Z | ||
3d7d195 | 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:24:37Z | ||
1dcf434 | 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-29T15:11:14Z | ||
9e5958d | 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 | 13 | 2023-12-02T20:30:58Z | ||
41fafea | 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) | 29 | 2023-11-30T22:37:35Z | ||
1d6d480 | 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 | 10 | 2023-11-29T00:56:59Z | ||
a4a92c4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:41:24+01:00 | ||
31a1ba2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T07:34:07Z | ||
31854c3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 9 | 2023-12-02T12:55:53Z | ||
5e630a0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2023-11-29T11:48:24Z | ||
49c8d72 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 9 | 2023-12-03T00:18:00Z | ||
ba64bee | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-19T15:09:48+01:00 | 7b5d7a4 | |
0e54b1f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-19T04:20:36+01:00 | e431567 | |
30ccb88 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-17T06:16:50+01:00 | 1fd351b | |
11728c5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-04T11:49:14+01:00 | 31854c3 | |
e37c83f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-04T02:02:18+01:00 | 9d147f7 | |
2be7e92 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-03T18:29:42+01:00 | a4a92c4 | |
960c3fa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-03T09:54:32+01:00 | 31a1ba2 | |
2103e03 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-03T06:05:28+01:00 | 49c8d72 | |
ae80952 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T11:50:55+01:00 | bafb422 | |
bafb422 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T07:30:19+01:00 | ||
4e8d2a8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-29T18:26:50+01:00 | 5e630a0 | |
40789ad | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-29T08:07:19+01:00 | ddb36d1 | |
9d147f7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 5 | 2023-12-03T22:09:50+01:00 | ||
1fd351b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 5 | 2023-12-17T03:45:54+01:00 | ||
e431567 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2023-12-18T18:40:56+01:00 | ||
ddb36d1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 9 | 2023-11-29T01:11:56Z | ||
add3e0d | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 6d672be7-36fc-44f9-8005-9e328792b166 creation_time: '2023-11-29T02:11:56+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ba09afab-848d-475b-80b5-f0a31b48de7f/sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ba09afab-848d-475b-80b5-f0a31b48de7f/sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca.i : ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-29T07:44:13+01:00 | ||
f52fdaa | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 4550f7b1-056b-4f69-be88-500f516c3d04 creation_time: 2023-12-03T01:18+01:00 producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_049b0fbb-b619-473d-8f4f-8885cd81b7d5/sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_049b0fbb-b619-473d-8f4f-8885cd81b7d5/sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca.i : ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T05:46:10+01:00 | ||
170b79c | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 01ea014f-c5fc-4090-8de3-1d58dc1d630b creation_time: '2023-12-02T13:55:53+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_57f527c3-9934-400c-abba-3ff7945c92f1/sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_57f527c3-9934-400c-abba-3ff7945c92f1/sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca.i : ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-04T12:02:46+01:00 | ||
9e6cd54 | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 987877d3-5518-4ee9-a5e2-8d52373530e1 creation_time: 2023-12-01T01:49:17Z 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/HarrisLalNoriRajamani-2010SAS-Fig3-alloca.i''' task: input_files: - ../../sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca.i input_file_hashes: ../../sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca.i: ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: [] | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-01T04:27:29+01:00 |
Found 31 witnesses for program sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i, ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
47dc9d1 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:47:21+01:00 | ||
a5ca0b2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T14:22:14+01:00 | 47dc9d1 | |
61945df | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 5 | 2022-12-10T21:42:12+01:00 | ||
c48a08b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 6 | 2022-12-12T00:18:34+01:00 | ||
bb50dc3 | 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 | 10 | 2022-12-14T07:25:24Z | ||
50b0458 | 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-11T08:53:42Z | ||
4b6befe | 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 | 12 | 2022-12-14T23:38:16Z | ||
7417c79 | 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 | 10 | 2022-12-13T14:54:02Z | ||
a7f3712 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2022-12-09T17:34:03+01:00 | ||
ae8bd1b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T22:03:54+01:00 | ||
f73f6d2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T13:07:38Z | ||
f7454ed | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 9 | 2022-12-14T13:11:02Z | ||
5da6a76 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2022-12-11T09:23:10Z | ||
845996b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 9 | 2022-12-14T17:07:11Z | ||
fafe921 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T11:06:04+01:00 | f7454ed | |
66d09a9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T07:17:10+01:00 | 658c042 | |
c441748 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T06:23:30+01:00 | 845996b | |
7517817 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T03:52:19+01:00 | 5da6a76 | |
1bcc368 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T02:47:55+01:00 | 54cfb69 | |
85b0136 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T00:07:05+01:00 | 980719f | |
5034f1e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T22:52:36+01:00 | ae8bd1b | |
e685d26 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T18:33:14+01:00 | a936990 | |
ed57a42 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T17:38:39+01:00 | f73f6d2 | |
1825a94 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T11:55:40+01:00 | 547d818 | |
c5c4a57 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T00:30:43+01:00 | 91ac5f1 | |
547d818 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2022-12-10T17:38:28+01:00 | ||
54cfb69 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 5 | 2022-12-12T00:01:11+01:00 | ||
91ac5f1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 5 | 2022-12-25T12:41:57+01:00 | ||
a936990 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2022-12-10T00:10:59+01:00 | ||
658c042 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 9 | 2022-12-13T11:21:28Z | ||
0bdabea | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2022-12-08T16:20:26Z |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i, ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc.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/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i, ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc.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/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i, ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc.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/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i, ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc.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/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i, ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3cdb007 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 6 | 2017-12-01T18:37 CET (sv-comp) | ||
c39cd40 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 15 | 2017-12-01T15:00 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i, ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |