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 (0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0, sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i).

Found 27 witnesses for program sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i, 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 67b10c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness crux-llvm-0.5.0.99 5 2023-12-18T05:09:37+01:00
Download e3d1f14 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Taipan 8 2023-12-02T15:27:09Z
Download bc6f79c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 3 2023-11-29T17:06:33Z
Download 8b8f5af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 7.4.0 kind 4 2023-12-01T16:45:31Z
Download d41bb52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CBMC 5 2023-12-17T18:05:16+01:00
Download 07daada Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Bubaak 3 2023-12-05T12:27:15Z
Download e1aaf5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Automizer 8 2023-11-29T03:27:21Z
Download 518fa38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:37:54+01:00
Download 72bd4a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2023-12-03T06:59:16Z
Download d05dd8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-19T15:34:49+01:00 Download a3f8971
Download ed28ab4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-19T04:03:35+01:00 Download ca48a93
Download 7b6ac66 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-18T06:10:09+01:00 Download 67b10c0
Download 3a33e31 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-17T22:09:43+01:00 Download d41bb52
Download 62a7481 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-05T14:36:33+01:00 Download 07daada
Download 71faa5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T12:15:23+01:00 Download e3d1f14
Download 47ae616 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T02:02:41+01:00 Download 0396172
Download 238436d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T18:32:19+01:00 Download 518fa38
Download 7fee101 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T09:54:33+01:00 Download 72bd4a2
Download 7caf10c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-01T18:28:40+01:00 Download 8b8f5af
Download 0b36ec1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T12:40:13+01:00 Download 59a06b5
Download 59a06b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T07:44:08+01:00
Download 14fe72d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T03:06:08+01:00 Download bc6f79c
Download 7d49bcb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-29T08:36:14+01:00 Download e1aaf5e
Download 0396172 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 5 2023-12-03T22:15:25+01:00
Download ca48a93 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2023-12-18T22:05:39+01:00
Download 7d289e3 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: 8524fe1b-10f5-4d76-b04a-aa6cb7173da6 creation_time: 2023-12-01T01:57:45Z 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/ex1-alloca.i''' task: input_files: - ../../sv-benchmarks/c/termination-memory-alloca/ex1-alloca.i input_file_hashes: ../../sv-benchmarks/c/termination-memory-alloca/ex1-alloca.i: 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-alloca/ex1-alloca.i file_hash: 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0 line: 556 column: 11 function: test_fun value: 1 == r format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-alloca/ex1-alloca.i file_hash: 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0 line: 556 column: 11 function: test_fun value: r == 1 format: c_expression correctness_witness CPAchecker 2.3 6 2023-12-01T05:20:32+01:00
Download 58bc4e2 Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow constraint: format: C value: \result == 46341 location: column: 41 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_425bc055-4efa-457e-b4f7-091fb1f18826/sv-benchmarks/c/termination-memory-alloca/ex1-alloca.i line: 563 type: function_return - segment: - waypoint: action: follow constraint: format: C value: \result == 2 location: column: 65 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_425bc055-4efa-457e-b4f7-091fb1f18826/sv-benchmarks/c/termination-memory-alloca/ex1-alloca.i line: 563 type: function_return - segment: - waypoint: action: follow constraint: format: C value: \result == 0 location: column: 89 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_425bc055-4efa-457e-b4f7-091fb1f18826/sv-benchmarks/c/termination-memory-alloca/ex1-alloca.i line: 563 type: function_return - segment: - waypoint: action: follow location: column: 9 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_425bc055-4efa-457e-b4f7-091fb1f18826/sv-benchmarks/c/termination-memory-alloca/ex1-alloca.i line: 557 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T17:06:33Z' format_version: '0.1' producer: name: symbiotic task: data_model: LP64 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_425bc055-4efa-457e-b4f7-091fb1f18826/sv-benchmarks/c/termination-memory-alloca/ex1-alloca.i : 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_425bc055-4efa-457e-b4f7-091fb1f18826/sv-benchmarks/c/termination-memory-alloca/ex1-alloca.i language: C specification: CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-11-30T03:00:38+01:00

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

Trying to find witnesses for program (0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0, sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i).

Found 29 witnesses for program sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i, 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 76793c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness crux-llvm-0.5.0.99 5 2022-12-09T04:46:05+01:00
Download 9edef66 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Taipan 8 2022-12-14T06:54:52Z
Download 5d62c30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 3 2022-12-12T12:25:54Z
Download 54ce536 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Kojak 8 2022-12-14T16:55:30Z
Download d623941 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 7.0.0 kind 4 2022-12-18T15:47:27Z
Download ec3d456 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 6.8.0 kind 4 2022-12-25T11:27:31Z
Download 792ad6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 10 2023-01-29T10:44:35+01:00 Download 9edef66
Download d580937 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 10 2023-01-29T06:53:33+01:00 Download ebc7772
Download 1d78ff6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CBMC 5 2022-12-08T10:43:19+01:00
Download cd7f7cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Bubaak 3 2022-12-08T21:48:17Z
Download ebc7772 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Automizer 8 2022-12-13T21:13:07Z
Download 609e93c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:01:37+01:00
Download 9507f27 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2022-12-09T13:20:04Z
Download 16b5e0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T06:38:43+01:00 Download 54ce536
Download 93da184 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T05:58:29+01:00 Download 5d62c30
Download 552b614 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T02:34:02+01:00 Download 37d6913
Download 8bd2207 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T00:52:44+01:00 Download baadefd
Download ee0a6f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T22:53:21+01:00 Download 609e93c
Download 4e38f6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T18:38:42+01:00 Download 5903754
Download fc1665e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T17:38:45+01:00 Download 9507f27
Download 675618f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T15:42:12+01:00 Download d623941
Download 273aa33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T11:28:49+01:00 Download 1127ed2
Download 70a0686 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T08:35:17+01:00 Download 76793c3
Download dddc438 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T04:23:28+01:00 Download 1d78ff6
Download a6df91f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T02:25:30+01:00 Download ec3d456
Download 043eb64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T00:29:13+01:00 Download cd7f7cf
Download 1127ed2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2022-12-10T18:37:44+01:00
Download 37d6913 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 5 2022-12-12T01:59:21+01:00
Download 5903754 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2022-12-09T23:36:50+01:00

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

Trying to find witnesses for program (0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0, sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i).

Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i, 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 92e4f8b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2021-12-10T16:21:19

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

Trying to find witnesses for program (0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0, sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i).

Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i, 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 49dedd9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T22:40:21
Download 58eab5f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-09T00:10:50

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

Trying to find witnesses for program (0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0, sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i).

Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i, 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0.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 (0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0, sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i).

Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i, 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0.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 (0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0, sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i).

Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i, 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0d900a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 6 2017-12-01T18:15 CET (sv-comp)
Download b4c6d35 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 29 2017-12-01T16:40 CET (sv-comp)

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

Trying to find witnesses for program (0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0, sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i).

Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i, 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0.json

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