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 (30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827, sv-benchmarks/c/termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c).

Found 28 witnesses for program sv-benchmarks/c/termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c, 30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download aa99364 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T06:58:31Z
Download 0795bb0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:43:39+01:00
Download 0e0d976 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download e1d80f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 8 2023-12-02T11:37:13Z
Download d242e0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 8 2023-12-02T23:00:48Z
Download 2823ff6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-20T03:41:11+01:00 Download 0e0d976
Download 3c3bfd2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-19T14:28:58+01:00 Download 5a9c2c1
Download efe31cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-19T04:04:29+01:00 Download 96b5d62
Download 0b67e80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-17T06:10:31+01:00 Download 0332f99
Download 1e0d552 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-04T11:50:30+01:00 Download e1d80f6
Download 2fceff9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-04T01:32:02+01:00 Download 53fb020
Download e83cd11 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-03T18:29:57+01:00 Download 0795bb0
Download 762c212 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-03T10:00:51+01:00 Download aa99364
Download fc9ef8f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-03T05:47:32+01:00 Download d242e0a
Download 17d45fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-01T00:03:35+01:00 Download 109502e
Download 0ad44d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-30T13:06:12+01:00 Download 15132c0
Download 15132c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-30T05:29:26+01:00
Download fa3d6dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-29T08:18:17+01:00 Download 995ecf0
Download 53fb020 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 4 2023-12-03T21:13:03+01:00
Download 0332f99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2023-12-17T02:12:58+01:00
Download 96b5d62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2023-12-19T02:13:48+01:00
Download 995ecf0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 8 2023-11-29T01:51:51Z
Download 109502e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 8 2023-11-30T20:59:41+01:00
Download b771e9d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 6 2023-11-30T20:43:53+01:00
Download 361b675 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: a3f8581a-1202-4413-981e-5bb17daa1bd7 creation_time: '2023-12-03T00:00:49+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0316a6b3-f8f4-4b2e-912c-48eb2c528396/sv-benchmarks/c/termination-restricted-15/b.03_assume.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0316a6b3-f8f4-4b2e-912c-48eb2c528396/sv-benchmarks/c/termination-restricted-15/b.03_assume.c : 30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827 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_0316a6b3-f8f4-4b2e-912c-48eb2c528396/sv-benchmarks/c/termination-restricted-15/b.03_assume.c file_hash: 30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827 line: 9 column: 0 function: main value: (((x <= 2147483647) && (0 <= (y + 2147483648))) || ((0 <= ((x + y) + 2147483646)) && (x <= 2147483647))) format: c_expression correctness_witness CPAchecker 2.3 6 2023-12-03T05:44:53+01:00
Download 4ef8c6b Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 9f0bbd83-a98a-42c8-9755-92bcd1977b12 creation_time: '2023-12-02T12:37:13+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d27e4239-3da8-448b-b7f3-66b7c24ae896/sv-benchmarks/c/termination-restricted-15/b.03_assume.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d27e4239-3da8-448b-b7f3-66b7c24ae896/sv-benchmarks/c/termination-restricted-15/b.03_assume.c : 30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827 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_d27e4239-3da8-448b-b7f3-66b7c24ae896/sv-benchmarks/c/termination-restricted-15/b.03_assume.c file_hash: 30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827 line: 9 column: 0 function: main value: ((x <= 2147483647) && (0 <= (y + 2147483648))) format: c_expression correctness_witness CPAchecker 2.3 6 2023-12-04T12:01:36+01:00
Download b73c4ab Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 11a6568b-c651-4c1c-a51f-a533725e82dd creation_time: '2023-11-29T02:51:51+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0dc23484-9468-4cfe-8463-1118946698e7/sv-benchmarks/c/termination-restricted-15/b.03_assume.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0dc23484-9468-4cfe-8463-1118946698e7/sv-benchmarks/c/termination-restricted-15/b.03_assume.c : 30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827 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_0dc23484-9468-4cfe-8463-1118946698e7/sv-benchmarks/c/termination-restricted-15/b.03_assume.c file_hash: 30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827 line: 9 column: 0 function: main value: ((x <= 2147483647) && (0 <= (y + 2147483648))) format: c_expression correctness_witness CPAchecker 2.3 6 2023-11-29T07:46:28+01:00
Download e3727a6 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: bcd82d40-c506-4b33-ba81-f18fa469488c creation_time: 2023-12-01T01:01:29Z 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-restricted-15/b.03_assume.c''' task: input_files: - ../../sv-benchmarks/c/termination-restricted-15/b.03_assume.c input_file_hashes: ../../sv-benchmarks/c/termination-restricted-15/b.03_assume.c: 30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: [] correctness_witness CPAchecker 2.3 5 2023-12-01T04:07:14+01:00

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

Trying to find witnesses for program (30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827, sv-benchmarks/c/termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c).

Found 25 witnesses for program sv-benchmarks/c/termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c, 30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3591ada Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness verifuzz 3 2022-12-15T05:49:27+01:00
Download d182fdf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T11:49:18Z
Download 716a278 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:14:40+01:00
Download 0e0d976 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T11:02 CET (comp)
Download 17bf008 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 8 2022-12-14T07:15:50Z
Download c4eb23f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 8 2022-12-15T02:43:44Z
Download 4dd0aee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T11:32:13+01:00 Download 0e0d976
Download 00a85fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T11:04:08+01:00 Download 17bf008
Download 8c4177a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T07:39:23+01:00 Download 0826f44
Download 6c8482f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T06:26:52+01:00 Download c4eb23f
Download 6635a17 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T02:49:58+01:00 Download 782ddd0
Download 49da38b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T00:10:01+01:00 Download b26aeff
Download d09257a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T22:50:35+01:00 Download 716a278
Download 2670701 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T18:46:49+01:00 Download 8aa446b
Download b9c66e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T17:44:19+01:00 Download d182fdf
Download 0dda596 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T11:16:30+01:00 Download c1fd86e
Download f75fc52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T00:46:55+01:00 Download 91189a1
Download 513df50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-27T23:08:31+01:00 Download 0067a3f
Download c1fd86e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2022-12-10T21:21:41+01:00
Download 782ddd0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 4 2022-12-12T01:27:17+01:00
Download 91189a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2022-12-25T09:42:12+01:00
Download 8aa446b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2022-12-10T03:17:19+01:00
Download 0826f44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 8 2022-12-13T19:32:56Z
Download 0067a3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 8 2022-12-08T01:23:10+01:00
Download ab66c62 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 6 2022-12-07T23:18:17+01:00

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

Trying to find witnesses for program (30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827, sv-benchmarks/c/termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c).

Found 1 witnesses for program sv-benchmarks/c/termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c, 30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 830d09f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 6 2021-12-05T22:18:08+01:00

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

Trying to find witnesses for program (30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827, sv-benchmarks/c/termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c, 30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827.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 '20

Trying to find witnesses for program (30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827, sv-benchmarks/c/termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c, 30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827.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 (30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827, sv-benchmarks/c/termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c, 30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827.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 (30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827, sv-benchmarks/c/termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c).

Found 2 witnesses for program sv-benchmarks/c/termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c, 30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download dde9860 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 4 2017-12-01T19:30 CET (sv-comp)
Download 72dbfd3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 7 2017-12-01T14:48 CET (sv-comp)

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

Trying to find witnesses for program (30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827, sv-benchmarks/c/termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c, 30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/30d70cf2197e08977a52494fd2970e41435b4a438b2b1792b181b4b6cf10a827.json

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