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 35 witnesses for program sv-benchmarks/c/termination-recursive-malloc/mutual_simple_true-termination.c.i, 6c12f09591910c75ee0fb408a48b3499b101134bf1227e2b3b797b62a89d1275
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/6c12f09591910c75ee0fb408a48b3499b101134bf1227e2b3b797b62a89d1275.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d0f6406 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T09:03:17+01:00 | ||
5097d87 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-18T12:01:04+01:00 | d0f6406 | |
714982e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T06:56:26+01:00 | ||
7ea51c9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 6 | 2023-12-03T21:26:20+01:00 | ||
2e971fb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 6 | 2023-12-17T02:11:46+01:00 | ||
b0e0889 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 6 | 2023-12-19T12:36:20+01:00 | ||
343918a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2023-12-18T21:19:04+01:00 | ||
306eec3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 7 | 2023-12-18T01:46:30+01:00 | ||
d302958 | 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 | 11 | 2023-12-02T11:40:18Z | ||
fe92c09 | 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 | 11 | 2023-12-02T21:29:57Z | ||
1dd350e | 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 | 11 | 2023-11-29T05:50:44Z | ||
d61ca06 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T04:22:36Z | ||
bc4ae70 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.1 | 4 | 2023-12-17T04:07:41+01:00 | ||
420fbc5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.0 | 4 | 2023-12-19T12:45:59+01:00 | ||
f146646 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 4 | 2023-12-18T23:22:48+01:00 | ||
6086c2f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:59:54+01:00 | ||
30e7e8d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 9 | 2023-12-02T15:56:40Z | ||
ff2c84e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 9 | 2023-12-03T03:39:56Z | ||
5608754 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-19T15:33:10+01:00 | 420fbc5 | |
372842f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-19T05:26:50+01:00 | f146646 | |
bce5578 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-17T06:40:59+01:00 | bc4ae70 | |
0e87cfc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-04T11:42:59+01:00 | 30e7e8d | |
e6012f5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-04T01:34:47+01:00 | 3d32f51 | |
4ab32c5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T18:31:03+01:00 | 6086c2f | |
e195a4a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T10:00:32+01:00 | d61ca06 | |
357a55b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T05:47:33+01:00 | ff2c84e | |
a95efe7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T12:42:18+01:00 | 46b9102 | |
46b9102 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T05:53:34+01:00 | ||
98f59c6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-29T08:14:36+01:00 | fd02cbc | |
3d32f51 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 5 | 2023-12-04T00:36:39+01:00 | ||
fd02cbc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 9 | 2023-11-28T23:01:47Z | ||
4a12ba0 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: c7eab741-d00e-4b02-9823-37d70fedea43 creation_time: '2023-11-29T00:01:47+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2c271780-303d-45e9-965f-7010debf56cb/sv-benchmarks/c/termination-recursive-malloc/mutual_simple.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2c271780-303d-45e9-965f-7010debf56cb/sv-benchmarks/c/termination-recursive-malloc/mutual_simple.i : 6c12f09591910c75ee0fb408a48b3499b101134bf1227e2b3b797b62a89d1275 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-29T07:46:36+01:00 | ||
33e395b | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 752a4684-f6db-42b6-ac4a-536ebb070393 creation_time: '2023-12-03T04:39:56+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_95d1ae95-f20e-4801-86b0-d7972a4009e8/sv-benchmarks/c/termination-recursive-malloc/mutual_simple.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_95d1ae95-f20e-4801-86b0-d7972a4009e8/sv-benchmarks/c/termination-recursive-malloc/mutual_simple.i : 6c12f09591910c75ee0fb408a48b3499b101134bf1227e2b3b797b62a89d1275 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T05:41:56+01:00 | ||
17dda80 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 3f4c8439-e65c-4a03-b54d-00eb55fdfa0e creation_time: '2023-12-02T16:56:40+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5ac1e4b5-72d4-4cbf-842f-5869080dc88e/sv-benchmarks/c/termination-recursive-malloc/mutual_simple.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5ac1e4b5-72d4-4cbf-842f-5869080dc88e/sv-benchmarks/c/termination-recursive-malloc/mutual_simple.i : 6c12f09591910c75ee0fb408a48b3499b101134bf1227e2b3b797b62a89d1275 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-04T12:02:17+01:00 | ||
8031aa9 | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 91b5bcef-6d71-4c7b-9fa6-46bffeb648dd creation_time: 2023-12-01T02:01:03Z 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-recursive-malloc/mutual_simple.i''' task: input_files: - ../../sv-benchmarks/c/termination-recursive-malloc/mutual_simple.i input_file_hashes: ../../sv-benchmarks/c/termination-recursive-malloc/mutual_simple.i: 6c12f09591910c75ee0fb408a48b3499b101134bf1227e2b3b797b62a89d1275 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: [] | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-01T05:25:46+01:00 |
Found 32 witnesses for program sv-benchmarks/c/termination-recursive-malloc/mutual_simple_true-termination.c.i, 6c12f09591910c75ee0fb408a48b3499b101134bf1227e2b3b797b62a89d1275
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/6c12f09591910c75ee0fb408a48b3499b101134bf1227e2b3b797b62a89d1275.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e1b3691 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T05:11:50+01:00 | ||
9bec89f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T14:16:01+01:00 | e1b3691 | |
85260c4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 6 | 2022-12-10T16:57:54+01:00 | ||
cf5ec30 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 6 | 2022-12-12T01:30:34+01:00 | ||
a5c7619 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 6 | 2022-12-25T09:58:26+01:00 | ||
99f4890 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 7 | 2022-12-09T02:24:30+01:00 | ||
52dd6ac | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2022-12-10T02:05:08+01:00 | ||
7d7d182 | 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 | 11 | 2022-12-14T14:52:44Z | ||
f4b606b | 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 | 11 | 2022-12-14T18:21:48Z | ||
b704e45 | 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 | 11 | 2022-12-13T17:34:45Z | ||
121fd74 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0 | 6 | 2022-12-11T03:31:07+01:00 | ||
e7206d1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | verifuzz | 2 | 2022-12-15T09:13:40+01:00 | ||
c2c8991 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T11:31:58Z | ||
c310565 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.1 | 4 | 2022-12-25T11:20:42+01:00 | ||
1410568 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.0 | 4 | 2022-12-11T05:01:17+01:00 | ||
df61da8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 4 | 2022-12-09T17:11:29+01:00 | ||
2305558 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-11T01:54:40+01:00 | ||
ddb8fdb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 9 | 2022-12-14T08:34:35Z | ||
a7864fa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 9 | 2022-12-14T20:14:11Z | ||
43ec552 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T10:51:36+01:00 | ddb8fdb | |
111d3f8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T07:17:36+01:00 | 8fdb807 | |
0e2322c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T06:23:43+01:00 | a7864fa | |
dddaad4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T02:33:25+01:00 | 2da6ee9 | |
dfcb0af | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T00:54:38+01:00 | 1410568 | |
a2aa7c6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T22:51:19+01:00 | 2305558 | |
1619e5d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T21:08:18+01:00 | df61da8 | |
9e8bcfa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T17:45:31+01:00 | c2c8991 | |
9bf26b9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T11:38:22+01:00 | 966f156 | |
1b878d5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T02:22:52+01:00 | c310565 | |
966f156 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2022-12-10T17:28:06+01:00 | ||
2da6ee9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 5 | 2022-12-11T20:19:54+01:00 | ||
8fdb807 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 9 | 2022-12-13T17:30:46Z |
Found 1 witnesses for program sv-benchmarks/c/termination-recursive-malloc/mutual_simple_true-termination.c.i, 6c12f09591910c75ee0fb408a48b3499b101134bf1227e2b3b797b62a89d1275
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/6c12f09591910c75ee0fb408a48b3499b101134bf1227e2b3b797b62a89d1275.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f81eab8 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T17:53:43 |
Found 2 witnesses for program sv-benchmarks/c/termination-recursive-malloc/mutual_simple_true-termination.c.i, 6c12f09591910c75ee0fb408a48b3499b101134bf1227e2b3b797b62a89d1275
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/6c12f09591910c75ee0fb408a48b3499b101134bf1227e2b3b797b62a89d1275.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
bb2210d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T17:01:10 | ||
75a88b0 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-09T00:58:19 |
Found 0 witnesses for program sv-benchmarks/c/termination-recursive-malloc/mutual_simple_true-termination.c.i, 6c12f09591910c75ee0fb408a48b3499b101134bf1227e2b3b797b62a89d1275
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/6c12f09591910c75ee0fb408a48b3499b101134bf1227e2b3b797b62a89d1275.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-recursive-malloc/mutual_simple_true-termination.c.i, 6c12f09591910c75ee0fb408a48b3499b101134bf1227e2b3b797b62a89d1275
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6c12f09591910c75ee0fb408a48b3499b101134bf1227e2b3b797b62a89d1275.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 1 witnesses for program sv-benchmarks/c/termination-recursive-malloc/mutual_simple_true-termination.c.i, 6c12f09591910c75ee0fb408a48b3499b101134bf1227e2b3b797b62a89d1275
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/6c12f09591910c75ee0fb408a48b3499b101134bf1227e2b3b797b62a89d1275.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c6984a8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 6 | 2017-12-01T19:53 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-recursive-malloc/mutual_simple_true-termination.c.i, 6c12f09591910c75ee0fb408a48b3499b101134bf1227e2b3b797b62a89d1275
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/6c12f09591910c75ee0fb408a48b3499b101134bf1227e2b3b797b62a89d1275.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |