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 (eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30, sv-benchmarks/c/termination-memory-linkedlists/ll_search-alloca_true-termination.c.i).

Found 26 witnesses for program sv-benchmarks/c/termination-memory-linkedlists/ll_search-alloca_true-termination.c.i, eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 97194f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T18:00:11+01:00
Download d257842 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2023-12-03T04:16:10Z
Download 0a923f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 15 2023-12-02T18:48:24Z
Download 76f4142 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T16:07:40Z
Download 3169c3a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 51 2023-12-01T01:43:14Z
Download e767645 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-19T15:14:50+01:00 Download 77abf91
Download 8a0ab63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-19T03:14:29+01:00 Download 6b0f788
Download f81930a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-17T06:09:31+01:00 Download 827debf
Download 638b5b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-04T11:27:51+01:00 Download 0a923f9
Download c341fe3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-04T01:58:29+01:00 Download 909f594
Download c840e8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-03T18:30:37+01:00 Download 97194f8
Download cf3e252 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-03T09:54:04+01:00 Download d257842
Download 78b81bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-01T03:44:24+01:00 Download 3169c3a
Download dae9b34 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-30T23:57:29+01:00 Download 57e34f8
Download 9dd3c92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-30T12:07:01+01:00 Download bba353a
Download bba353a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-30T07:35:27+01:00
Download 3a3a3d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-29T18:13:38+01:00 Download 76f4142
Download a9b2049 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-29T07:51:48+01:00 Download c2c4153
Download 909f594 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 8 2023-12-03T21:40:46+01:00
Download 827debf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 8 2023-12-17T02:05:17+01:00
Download 6b0f788 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 8 2023-12-18T22:34:09+01:00
Download c2c4153 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 15 2023-11-29T00:12:02Z
Download 57e34f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 32 2023-11-30T20:41:59+01:00
Download 3a962af Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: af92492d-242b-4ce7-af13-a303acc3123c creation_time: '2023-11-29T01:12:02+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f16c446f-8da1-424c-973d-2c57b2f03754/sv-benchmarks/c/termination-memory-linkedlists/ll_search-alloca.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f16c446f-8da1-424c-973d-2c57b2f03754/sv-benchmarks/c/termination-memory-linkedlists/ll_search-alloca.i : eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f16c446f-8da1-424c-973d-2c57b2f03754/sv-benchmarks/c/termination-memory-linkedlists/ll_search-alloca.i file_hash: eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30 line: 550 column: 0 function: init_ll value: ((((n <= 2147483647) && (1 <= i)) && (n <= 2147483647)) || (((n <= 2147483647) && (i == 0)) && (n <= 2147483647))) format: c_expression correctness_witness CPAchecker 2.3 9 2023-11-29T07:45:10+01:00
Download 3cc8a34 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 04657956-43ae-4cad-af1b-30c4b7235881 creation_time: '2023-12-02T19:48:24+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_78df32a7-7dc0-490e-8215-d684eccd32f9/sv-benchmarks/c/termination-memory-linkedlists/ll_search-alloca.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_78df32a7-7dc0-490e-8215-d684eccd32f9/sv-benchmarks/c/termination-memory-linkedlists/ll_search-alloca.i : eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_78df32a7-7dc0-490e-8215-d684eccd32f9/sv-benchmarks/c/termination-memory-linkedlists/ll_search-alloca.i file_hash: eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30 line: 550 column: 0 function: init_ll value: ((((n <= 2147483647) && (1 <= i)) && (n <= 2147483647)) || (((n <= 2147483647) && (i == 0)) && (n <= 2147483647))) format: c_expression correctness_witness CPAchecker 2.3 9 2023-12-04T12:02:09+01:00
Download 205d42d Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: 4bf3374a-a807-4f1a-b468-2f63e04c3df0 creation_time: 2023-12-01T01:43:14Z 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-linkedlists/ll_search-alloca.i''' task: input_files: - ../../sv-benchmarks/c/termination-memory-linkedlists/ll_search-alloca.i input_file_hashes: ../../sv-benchmarks/c/termination-memory-linkedlists/ll_search-alloca.i: eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30 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-linkedlists/ll_search-alloca.i file_hash: eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30 line: 561 column: 9 function: safe_search value: 0 <= i format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-linkedlists/ll_search-alloca.i file_hash: eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30 line: 561 column: 9 function: safe_search value: i <= 2147483646 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-linkedlists/ll_search-alloca.i file_hash: eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30 line: 550 column: 6 function: init_ll value: n != 0 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-linkedlists/ll_search-alloca.i file_hash: eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30 line: 550 column: 6 function: init_ll value: (((0LL - (long long )i) + (long long )n >= 0LL && head == curr) && ((((((((7 <= n && 7 <= i) && (-14LL + (long long )i) + (long long )n >= 0LL) || ((6 <= n && (-12LL + (long long )i) + (long long )n >= 0LL) && i == 6)) || ((5 <= n && (-10LL + (long long )i) + (long long )n >= 0LL) && i == 5)) || ((4 <= n && (-8LL + (long long )i) + (long long )n >= 0LL) && i == 4)) || ((3 <= n && (-6LL + (long long )i) + (long long )n >= 0LL) && i == 3)) || ((2 <= n && (-4LL + (long long )i) + (long long )n >= 0LL) && i == 2)) || ((1 <= n && (-2LL + (long long )i) + (long long )n >= 0LL) && i == 1))) || (((((((1 <= n && (-1LL + (long long )i) + (long long )n >= 0LL) && (-1LL - (long long )i) + (long long )n >= 0LL) && 0 == head) && 0 == i) && head == 0) && head == i) && i == 0) format: c_expression correctness_witness CPAchecker 2.3 11 2023-12-01T04:46:16+01:00

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

Trying to find witnesses for program (eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30, sv-benchmarks/c/termination-memory-linkedlists/ll_search-alloca_true-termination.c.i).

Found 23 witnesses for program sv-benchmarks/c/termination-memory-linkedlists/ll_search-alloca_true-termination.c.i, eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d753345 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:06:02+01:00
Download 0858ddf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2022-12-09T09:54:30Z
Download c72471d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 13 2022-12-14T12:43:04Z
Download 0cc50df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T11:08:41Z
Download 68b3f90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp23-0-g4f5dcf38f) 85 2022-12-10T06:50:38Z
Download 1ed09cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T11:06:49+01:00 Download c72471d
Download b55f41f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T07:31:50+01:00 Download 1bb1a7d
Download ebdfacd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T03:48:21+01:00 Download 0cc50df
Download 7921437 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T03:11:40+01:00 Download 041061e
Download 40c444b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T00:06:26+01:00 Download f7874f4
Download a5a7d41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T22:51:49+01:00 Download d753345
Download 133b621 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T22:38:22+01:00 Download 68b3f90
Download b5352d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T18:22:34+01:00 Download 474278b
Download 5f05800 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T17:38:29+01:00 Download 0858ddf
Download 05e0cfb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T11:26:28+01:00 Download fb22d88
Download 93cf3ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T00:46:25+01:00 Download 47f2968
Download 529ca00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-27T23:08:15+01:00 Download 86bcc8e
Download fb22d88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2022-12-10T16:35:41+01:00
Download 041061e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 8 2022-12-12T01:07:44+01:00
Download 47f2968 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 8 2022-12-25T07:24:20+01:00
Download 474278b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 8 2022-12-10T03:17:16+01:00
Download 1bb1a7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 13 2022-12-13T13:00:19Z
Download 86bcc8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 32 2022-12-08T00:06:53+01:00

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

Trying to find witnesses for program (eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30, sv-benchmarks/c/termination-memory-linkedlists/ll_search-alloca_true-termination.c.i).

Found 1 witnesses for program sv-benchmarks/c/termination-memory-linkedlists/ll_search-alloca_true-termination.c.i, eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30.json

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

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

Trying to find witnesses for program (eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30, sv-benchmarks/c/termination-memory-linkedlists/ll_search-alloca_true-termination.c.i).

Found 2 witnesses for program sv-benchmarks/c/termination-memory-linkedlists/ll_search-alloca_true-termination.c.i, eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 76ae4c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T21:31:03
Download 5ff74bb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-08T14:06:49

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

Trying to find witnesses for program (eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30, sv-benchmarks/c/termination-memory-linkedlists/ll_search-alloca_true-termination.c.i).

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

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

Found 1 witnesses for program sv-benchmarks/c/termination-memory-linkedlists/ll_search-alloca_true-termination.c.i, eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30.json

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

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

Trying to find witnesses for program (eecb5727313c812036fce0f3f0f3b10c00629cd032f9c1c91d708595e629df30, sv-benchmarks/c/termination-memory-linkedlists/ll_search-alloca_true-termination.c.i).

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

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