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 (0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4, sv-benchmarks/c/termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 12 witnesses for program sv-benchmarks/c/termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c, 0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download cd6736a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T07:15:49Z
Download 581c845 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness VeriOover 2 2023-12-20T03:38 CET (comp)
Download a469388 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:49:03+01:00
Download e972ac0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-20T03:41:26+01:00 Download 581c845
Download 0890e00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 679 2023-12-03T18:47:29+01:00 Download a469388
Download 06b0cfb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 108 2023-12-03T10:01:34+01:00 Download cd6736a
Download 1d171bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 700 2023-11-30T07:05:34+01:00
Download d78ac53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 689 2023-12-03T22:55:57+01:00
Download df07c8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 679 2023-12-18T18:22:53+01:00
Download b9ef062 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 3 2023-12-01T02:10:56Z
Download 8b5909a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 7 2023-11-30T21:33:44+01:00
Download 6ceae76 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: 79cf53ae-f341-43b0-a283-d18b1bf2b604 creation_time: 2023-11-30T22:32:55Z 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-crafted/easy2-2.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted/easy2-2.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted/easy2-2.c: 0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/easy2-2.c file_hash: 0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4 line: 20 column: 8 function: main value: (long long )x + (long long )y >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/easy2-2.c file_hash: 0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4 line: 20 column: 8 function: main value: (0LL - (long long )x) - (long long )y >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/easy2-2.c file_hash: 0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4 line: 20 column: 8 function: main value: ((0 <= z && z != -1) && ((z != -2 && ((z != -3 && ((z != -4 && ((z != -5 && ((z != -6 && ((z != -7 && (((((((8 <= x && y <= -8) && z <= 2147483639) && (-8LL + (long long )x) + (long long )z >= 0LL) && (-8LL - (long long )y) + (long long )z >= 0LL) && (-16LL + (long long )x) - (long long )y >= 0LL) && z != -8) || ((((((((z <= 2147483640 && (-7LL + (long long )x) + (long long )z >= 0LL) && (7LL + (long long )y) + (long long )z >= 0LL) && (-7LL - (long long )y) + (long long )z >= 0LL) && (7LL - (long long )x) + (long long )z >= 0LL) && (14LL - (long long )x) + (long long )y >= 0LL) && (-14LL + (long long )x) - (long long )y >= 0LL) && x == 7) && y == -7))) || ((((((((z <= 2147483641 && (-6LL + (long long )x) + (long long )z >= 0LL) && (6LL + (long long )y) + (long long )z >= 0LL) && (-6LL - (long long )y) + (long long )z >= 0LL) && (6LL - (long long )x) + (long long )z >= 0LL) && (12LL - (long long )x) + (long long )y >= 0LL) && (-12LL + (long long )x) - (long long )y >= 0LL) && x == 6) && y == -6))) || ((((((((z <= 2147483642 && (-5LL + (long long )x) + (long long )z >= 0LL) && (5LL + (long long )y) + (long long )z >= 0LL) && (-5LL - (long long )y) + (long long )z >= 0LL) && (5LL - (long long )x) + (long long )z >= 0LL) && (10LL - (long long )x) + (long long )y >= 0LL) && (-10LL + (long long )x) - (long long )y >= 0LL) && x == 5) && y == -5))) || ((((((((z <= 2147483643 && (-4LL + (long long )x) + (long long )z >= 0LL) && (4LL + (long long )y) + (long long )z >= 0LL) && (-4LL - (long long )y) + (long long )z >= 0LL) && (4LL - (long long )x) + (long long )z >= 0LL) && (8LL - (long long )x) + (long long )y >= 0LL) && (-8LL + (long long )x) - (long long )y >= 0LL) && x == 4) && y == -4))) || ((((((((z <= 2147483644 && (-3LL + (long long )x) + (long long )z >= 0LL) && (3LL + (long long )y) + (long long )z >= 0LL) && (-3LL - (long long )y) + (long long )z >= 0LL) && (3LL - (long long )x) + (long long )z >= 0LL) && (6LL - (long long )x) + (long long )y >= 0LL) && (-6LL + (long long )x) - (long long )y >= 0LL) && x == 3) && y == -3))) || ((((((((z <= 2147483645 && (-2LL + (long long )x) + (long long )z >= 0LL) && (2LL + (long long )y) + (long long )z >= 0LL) && (-2LL - (long long )y) + (long long )z >= 0LL) && (2LL - (long long )x) + (long long )z >= 0LL) && (4LL - (long long )x) + (long long )y >= 0LL) && (-4LL + (long long )x) - (long long )y >= 0LL) && x == 2) && y == -2))) || ((((((((z <= 2147483646 && (-1LL + (long long )x) + (long long )z >= 0LL) && (1LL + (long long )y) + (long long )z >= 0LL) && (-1LL - (long long )y) + (long long )z >= 0LL) && (1LL - (long long )x) + (long long )z >= 0LL) && (2LL - (long long )x) + (long long )y >= 0LL) && (-2LL + (long long )x) - (long long )y >= 0LL) && x == 1) && y == -1))) || (((((((0LL - (long long )x) + (long long )y >= 0LL && (long long )x - (long long )y >= 0LL) && 0 == x) && 0 == y) && x == 0) && x == y) && y == 0) format: c_expression correctness_witness CPAchecker 2.3 629 2023-12-01T05:44:56+01:00

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

Trying to find witnesses for program (0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4, sv-benchmarks/c/termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 12 witnesses for program sv-benchmarks/c/termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c, 0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 253fa5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T12:06:29Z
Download 581c845 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness VeriOover 2 2022-12-12T10:58 CET (comp)
Download 080ec3b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:02:35+01:00
Download eb5e53c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T11:32:34+01:00 Download 581c845
Download 72faa4f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 661 2023-01-29T02:47:44+01:00 Download 76d9931
Download 0f68e29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 679 2023-01-28T23:07:27+01:00 Download 080ec3b
Download cd29d0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T17:45:22+01:00 Download 253fa5e
Download 58cee64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 751 2022-12-10T19:11:12+01:00
Download 76d9931 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 4 2022-12-12T01:21:10+01:00
Download b32e4b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 766 2022-12-10T03:00:56+01:00
Download 5ca09b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2022-12-08T15:07:02Z
Download 81247b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 7 2022-12-07T23:28:05+01:00

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

Trying to find witnesses for program (0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4, sv-benchmarks/c/termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 9 witnesses for program sv-benchmarks/c/termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c, 0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 39321f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.8 3 2021-12-13T20:02:33Z
Download 263ec87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 4 2021-12-05T20:20:28+01:00 Download 2e211f0
Download 9e35d07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2021-12-06T14:21:25+01:00
Download 56347a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 679 2021-12-09T16:07:49+01:00 Download 65f2e41
Download a011406 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-06T14:59:45+01:00 Download 9e35d07
Download 2e211f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 33 2021-12-05T14:30:08+01:00
Download 8e395c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 718 2021-12-08T18:37:29+01:00
Download 65f2e41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 4 2021-12-09T14:32:44+01:00
Download 0481201 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 7 2021-12-05T22:41:22+01:00

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

Trying to find witnesses for program (0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4, sv-benchmarks/c/termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 4 witnesses for program sv-benchmarks/c/termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c, 0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1727643 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.1 3 2020-12-06T23:26:45
Download 927fd8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) unknown_witness Goblint (svcomp21-0-g82e03b87) 3 2020-12-07T11:09:26
Download 09c6b37 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 722 2020-12-05T12:55:15+01:00
Download 0dbbfa4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 732 2020-12-08T00:13:06+01:00

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

Trying to find witnesses for program (0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4, sv-benchmarks/c/termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 4 witnesses for program sv-benchmarks/c/termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c, 0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c0c9c69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.9 4 2019-11-29T20:43:43+01:00
Download d42a843 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 4 2019-12-01T00:52:46+01:00
Download 549c272 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 4 2019-11-30T13:52:45+01:00
Download 2b96296 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 377 2019-12-01T01:35:53+01:00

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

Trying to find witnesses for program (0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4, sv-benchmarks/c/termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 3 witnesses for program sv-benchmarks/c/termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c, 0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 81f3b86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 1080 2018-12-06T20:25:18+01:00
Download d534fff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 1076 2018-12-06T07:17:08+01:00
Download 48cf48b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T08:17 CET (sv-comp)

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

Trying to find witnesses for program (0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4, sv-benchmarks/c/termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 3 witnesses for program sv-benchmarks/c/termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c, 0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d83df53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 7 2017-12-03T07:44Z
Download afeab0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 5 2017-12-01T15:58 CET (sv-comp)
Download 41d18be Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 8 2017-12-01T16:56 CET (sv-comp)

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

Trying to find witnesses for program (0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4, sv-benchmarks/c/termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c, 0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/0ba0e3ec7d24c78a29a4980275f3f450c6adf9cab13a788bc587b5f2c8c6cbd4.json

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