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 (e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869, sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i).

Found 30 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i, e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8c2e4c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T04:16:36Z
Download 5c37bec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness crux-llvm-0.5.0.99 4 2023-12-18T04:35:09+01:00
Download 88b771a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Taipan 5 2023-12-02T18:10:58Z
Download a74d7ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 3 2023-11-30T00:07:43Z
Download 91b6a5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Kojak 5 2023-12-03T01:59:13Z
Download 3e4a807 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 7.4.0 kind 4 2023-12-01T10:28:36Z
Download 5404d5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-19T05:28:24+01:00 Download c801ea3
Download 1c4e3f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-05T14:39:54+01:00 Download b359420
Download cf35dda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-04T16:44:52+01:00 Download 6844d18
Download 6e6e695 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-04T12:13:34+01:00 Download 88b771a
Download a5cb96a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-04T02:26:58+01:00 Download 8b50725
Download cc794ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-03T18:33:29+01:00 Download 67b1a00
Download 39296b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-03T09:56:51+01:00 Download 8c2e4c3
Download 5eea19f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-03T06:18:48+01:00 Download 91b6a5b
Download 02855de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-11-30T13:45:43+01:00 Download fce4c3f
Download fce4c3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-11-30T07:08:32+01:00
Download 821b77d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-11-30T03:03:55+01:00 Download a74d7ab
Download c66223a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-11-29T08:34:40+01:00 Download 994b7ac
Download 8b50725 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 5 2023-12-03T23:11:33+01:00
Download c801ea3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2023-12-19T01:09:47+01:00
Download e40f58e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CBMC 4 2023-12-17T08:39:17+01:00
Download b359420 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Bubaak 3 2023-12-05T10:45:53Z
Download 6844d18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Bubaak 3 2023-12-04T14:41:44Z
Download 994b7ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Automizer 5 2023-11-28T19:44:17Z
Download 67b1a00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:48:36+01:00
Download 8e78dea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-18T06:02:43+01:00 Download 5c37bec
Download 4b699a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-17T22:07:44+01:00 Download e40f58e
Download a038c16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-01T18:27:20+01:00 Download 3e4a807
Download db9d16e Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: 1b3fab0c-9618-4a4e-bb72-1296f783c67e creation_time: 2023-12-01T01:05:01Z 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/rec_malloc_ex8.i''' task: input_files: - ../../sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8.i input_file_hashes: ../../sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8.i: e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: [] violation_witness CPAchecker 2.3 6 2023-12-01T05:22:02+01:00
Download e45ed39 Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow constraint: format: C value: \result == 1 location: column: 30 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0637d806-5cbc-4042-b7b8-a658cc28c370/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8.i line: 44 type: function_return - segment: - waypoint: action: follow constraint: format: C value: \result == 2147483647 location: column: 30 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0637d806-5cbc-4042-b7b8-a658cc28c370/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8.i line: 45 type: function_return - segment: - waypoint: action: follow location: column: 5 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0637d806-5cbc-4042-b7b8-a658cc28c370/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8.i line: 13 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-30T00:07:43Z' format_version: '0.1' producer: name: symbiotic task: data_model: LP64 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0637d806-5cbc-4042-b7b8-a658cc28c370/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8.i : e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0637d806-5cbc-4042-b7b8-a658cc28c370/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8.i language: C specification: CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 7 2023-11-30T02:57:23+01:00

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

Trying to find witnesses for program (e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869, sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i).

Found 29 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i, e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5aafc45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness verifuzz 3 2022-12-15T12:11:22+01:00
Download 08d6c85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T10:02:42Z
Download 6ba141b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness crux-llvm-0.5.0.99 4 2022-12-09T03:42:49+01:00
Download 283fb4f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Taipan 5 2022-12-14T12:07:40Z
Download 6c0e8c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 3 2022-12-12T16:07:05Z
Download e45c95c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Kojak 5 2022-12-14T16:53:54Z
Download cebdabd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 7.0.0 kind 4 2022-12-19T02:41:50Z
Download b14c7f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 6.8.0 kind 4 2022-12-25T10:59:13Z
Download f88ddf8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-29T10:44:49+01:00 Download 283fb4f
Download f71d13f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-29T06:53:46+01:00 Download 0946bc9
Download a25fc1f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-29T06:38:00+01:00 Download e45c95c
Download 2c4d533 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-29T05:56:11+01:00 Download 6c0e8c8
Download b9cae5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-29T01:31:35+01:00 Download b56964c
Download b4207fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-28T22:50:52+01:00 Download cc235fa
Download 53c1148 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-28T21:04:32+01:00 Download 74f77d4
Download 570d62c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-28T17:48:06+01:00 Download 08d6c85
Download 6e6f7de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-28T15:42:19+01:00 Download cebdabd
Download 2b15b26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-28T08:55:30+01:00 Download c82b5f0
Download 17a3fa8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-28T02:22:24+01:00 Download b14c7f9
Download c82b5f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2022-12-10T21:46:01+01:00
Download b56964c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 5 2022-12-12T00:36:10+01:00
Download 74f77d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2022-12-10T00:26:43+01:00
Download 3227d7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CBMC 4 2022-12-08T11:12:36+01:00
Download 1b4f6d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Bubaak 3 2022-12-08T18:19:31Z
Download 0946bc9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Automizer 5 2022-12-13T11:36:27Z
Download cc235fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:17:12+01:00
Download 603e2f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T08:30:08+01:00 Download 6ba141b
Download 2362201 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T04:21:48+01:00 Download 3227d7a
Download 1fa9d32 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T00:29:59+01:00 Download 1b4f6d1

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

Trying to find witnesses for program (e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869, sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i).

Found 1 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i, e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2dce79f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2021-12-10T17:55:06

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

Trying to find witnesses for program (e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869, sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i).

Found 2 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i, e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0a839c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T18:37:12
Download dd2f3be Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-09T01:52:08

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

Trying to find witnesses for program (e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869, sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i).

Found 0 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i, e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869.json

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

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

Trying to find witnesses for program (e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869, sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i).

Found 0 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i, e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869.json

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

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

Trying to find witnesses for program (e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869, sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i).

Found 1 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i, e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1e8abca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 8 2017-12-01T20:28 CET (sv-comp)

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

Trying to find witnesses for program (e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869, sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i).

Found 0 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i, e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869.json

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