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).

View and Validate the Witness

Input Given to this Service about the Witness (URL Query)

Key Value
programName sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c
programSHA d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff
witnessName results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-termination.LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c.files/witness.graphml
witnessSHA b794319bb7473b5b269ab10dabdea98d9a2e7294402d9934a7aa111310fa4224

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/b794319bb7473b5b269ab10dabdea98d9a2e7294402d9934a7aa111310fa4224.json

Key Value
architecture 32bit
creationtime 2018-12-06T05:48:52.213485
producer DepthK v3.0
programfile /tmp/vcloud-vcloud-master/worker/working_dir_5db04296-c534-43fc-950c-2a309a2548b1/sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c
programhash b9dfe2826dbd43b76a93fbf593c8a07947a4c894
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/b794319bb7473b5b269ab10dabdea98d9a2e7294402d9934a7aa111310fa4224.graphml
witness-sha256 b794319bb7473b5b269ab10dabdea98d9a2e7294402d9934a7aa111310fa4224
witness-size 3521
witness-type correctness_witness

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

Trying to find witnesses for program (d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff, sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 28 witnesses for program sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c, d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f9b9995 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T10:56:18+01:00
Download b8ae4a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2023-12-17T00:52:12Z
Download 1eddf03 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2023-11-29T19:42:47Z
Download e4d3d55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 6 2023-11-30T02:38:55+01:00
Download 1b1e9be Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 6 2023-12-03T22:18:54+01:00
Download 50d108c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2023-12-18T22:10:32+01:00
Download 46cebb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 11 2023-12-02T17:32:39Z
Download fa3106e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 30 2023-12-01T01:34:42Z
Download 4777c81 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 11 2023-11-29T05:13:51Z
Download fd9bbac Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness 2LS 14 2023-11-30T23:21:17+01:00
Download a4dd829 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2023-12-03T06:29:49Z
Download 9a2f5f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:38 CET (comp)
Download 7b8c57e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 30 2023-12-01T02:09:31Z
Download ec747f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-20T03:41:10+01:00 Download 9a2f5f8
Download cc7567b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-19T15:11:24+01:00 Download 8678dcc
Download 6120fb6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-19T05:09:29+01:00 Download cc87841
Download ae4a4af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-17T06:24:20+01:00 Download 21ff1f4
Download 9e1653c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-04T01:50:05+01:00 Download 3d1c610
Download 1739ea4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-03T09:54:13+01:00 Download a4dd829
Download 6f3ee94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-01T03:36:37+01:00 Download 7b8c57e
Download 0acdec8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-01T00:04:55+01:00 Download 8ff7ad0
Download a067775 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-11-30T12:07:56+01:00 Download 8101f70
Download 8101f70 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-11-30T07:54:54+01:00
Download 3d1c610 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 6 2023-12-03T21:15:50+01:00
Download 21ff1f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2023-12-17T04:51:05+01:00
Download cc87841 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2023-12-18T20:12:36+01:00
Download 8ff7ad0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 12 2023-11-30T22:32:03+01:00
Download 104d01f Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: 05fe3eb6-9296-49e3-aa55-72329fb4939d creation_time: 2023-12-01T02:09:31Z 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/LexIndexValue-Array-1.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted/LexIndexValue-Array-1.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted/LexIndexValue-Array-1.c: d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff 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/LexIndexValue-Array-1.c file_hash: d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff line: 18 column: 8 function: main value: (-1048LL + (long long )i) + (long long )k >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/LexIndexValue-Array-1.c file_hash: d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff line: 18 column: 8 function: main value: (1048LL - (long long )i) + (long long )k >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/LexIndexValue-Array-1.c file_hash: d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff line: 18 column: 8 function: main value: i == 1048 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/LexIndexValue-Array-1.c file_hash: d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff line: 18 column: 8 function: main value: ((((((((0 <= k && (((((((k <= 3 && k <= 65535) && (-1045LL + (long long )i) - (long long )k >= 0LL) && (1051LL - (long long )i) - (long long )k >= 0LL) || (((k <= 2 && k <= 255) && (-1046LL + (long long )i) - (long long )k >= 0LL) && (1050LL - (long long )i) - (long long )k >= 0LL)) || (((k <= 2 && k <= 255) && (-1046LL + (long long )i) - (long long )k >= 0LL) && (1050LL - (long long )i) - (long long )k >= 0LL)) || (((k <= 1 && (-1047LL + (long long )i) - (long long )k >= 0LL) && (1049LL - (long long )i) - (long long )k >= 0LL) && (k == 0 || k == 1))) || (((k <= 1 && (-1047LL + (long long )i) - (long long )k >= 0LL) && (1049LL - (long long )i) - (long long )k >= 0LL) && (k == 0 || k == 1)))) || ((((-1048LL + (long long )i) - (long long )k >= 0LL && (1048LL - (long long )i) - (long long )k >= 0LL) && 0 == k) && k == 0)) || ((((-1048LL + (long long )i) - (long long )k >= 0LL && (1048LL - (long long )i) - (long long )k >= 0LL) && 0 == k) && k == 0)) || (((0 <= k && k <= 1047) && (-1LL + (long long )i) - (long long )k >= 0LL) && (2095LL - (long long )i) - (long long )k >= 0LL)) || (((0 <= k && k <= 1048) && (2096LL - (long long )i) - (long long )k >= 0LL) && (long long )i - (long long )k >= 0LL)) || (((0 <= k && k <= 5) && (-1043LL + (long long )i) - (long long )k >= 0LL) && (1053LL - (long long )i) - (long long )k >= 0LL)) || (((0 <= k && k <= 5) && (-1043LL + (long long )i) - (long long )k >= 0LL) && (1053LL - (long long )i) - (long long )k >= 0LL)) || (((0 <= k && k <= 4) && (-1044LL + (long long )i) - (long long )k >= 0LL) && (1052LL - (long long )i) - (long long )k >= 0LL)) || (((0 <= k && k <= 4) && (-1044LL + (long long )i) - (long long )k >= 0LL) && (1052LL - (long long )i) - (long long )k >= 0LL) format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/LexIndexValue-Array-1.c file_hash: d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff line: 14 column: 6 function: main value: 0 == k format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/LexIndexValue-Array-1.c file_hash: d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff line: 14 column: 6 function: main value: k == 0 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/LexIndexValue-Array-1.c file_hash: d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff line: 14 column: 6 function: main value: ((((((((((((8 <= i && i <= 1048) && (-8LL + (long long )i) + (long long )k >= 0LL) && (1048LL - (long long )i) + (long long )k >= 0LL) && (-8LL + (long long )i) - (long long )k >= 0LL) && (1048LL - (long long )i) - (long long )k >= 0LL) || (((((-7LL + (long long )i) + (long long )k >= 0LL && (7LL - (long long )i) + (long long )k >= 0LL) && (-7LL + (long long )i) - (long long )k >= 0LL) && (7LL - (long long )i) - (long long )k >= 0LL) && i == 7)) || (((((-6LL + (long long )i) + (long long )k >= 0LL && (6LL - (long long )i) + (long long )k >= 0LL) && (-6LL + (long long )i) - (long long )k >= 0LL) && (6LL - (long long )i) - (long long )k >= 0LL) && i == 6)) || (((((-5LL + (long long )i) + (long long )k >= 0LL && (5LL - (long long )i) + (long long )k >= 0LL) && (-5LL + (long long )i) - (long long )k >= 0LL) && (5LL - (long long )i) - (long long )k >= 0LL) && i == 5)) || (((((-4LL + (long long )i) + (long long )k >= 0LL && (4LL - (long long )i) + (long long )k >= 0LL) && (-4LL + (long long )i) - (long long )k >= 0LL) && (4LL - (long long )i) - (long long )k >= 0LL) && i == 4)) || (((((-3LL + (long long )i) + (long long )k >= 0LL && (3LL - (long long )i) + (long long )k >= 0LL) && (-3LL + (long long )i) - (long long )k >= 0LL) && (3LL - (long long )i) - (long long )k >= 0LL) && i == 3)) || (((((-2LL + (long long )i) + (long long )k >= 0LL && (2LL - (long long )i) + (long long )k >= 0LL) && (-2LL + (long long )i) - (long long )k >= 0LL) && (2LL - (long long )i) - (long long )k >= 0LL) && i == 2)) || (((((-1LL + (long long )i) + (long long )k >= 0LL && (1LL - (long long )i) + (long long )k >= 0LL) && (-1LL + (long long )i) - (long long )k >= 0LL) && (1LL - (long long )i) - (long long )k >= 0LL) && i == 1)) || (((((((0LL - (long long )i) + (long long )k >= 0LL && (long long )i + (long long )k >= 0LL) && (0LL - (long long )i) - (long long )k >= 0LL) && (long long )i - (long long )k >= 0LL) && 0 == i) && k == i) && i == 0) format: c_expression correctness_witness CPAchecker 2.3 14 2023-12-01T05:38:57+01:00

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

Trying to find witnesses for program (d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff, sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 25 witnesses for program sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c, d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 947b2ea Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T06:48:06+01:00
Download 118a240 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2022-12-25T10:24:17Z
Download f68b6c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 6 2022-12-10T17:19:21+01:00
Download ab1ca0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 6 2022-12-12T00:54:37+01:00
Download 748c148 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2022-12-10T00:23:25+01:00
Download 8b6d3d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 11 2022-12-14T15:03:34Z
Download 171361e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 10 2022-12-13T19:03:52Z
Download e235d86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness 2LS 14 2022-12-07T21:36:22+01:00
Download 99300f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 2 2023-01-28T22:42:29+01:00 Download c07073a
Download fbbe451 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2022-12-09T09:59:38Z
Download 9a2f5f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T10:59 CET (comp)
Download c07073a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp23-0-g4f5dcf38f) 61 2022-12-10T08:38:14Z
Download e05fe4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T11:32:18+01:00 Download 9a2f5f8
Download 24d611c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T03:03:10+01:00 Download 0cfdf42
Download 31e87b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T00:07:14+01:00 Download bd41467
Download cb76093 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-28T19:01:20+01:00 Download 7dc3f2c
Download eaf0f5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-28T17:38:33+01:00 Download fbbe451
Download d583398 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-28T10:53:16+01:00 Download b9aefe8
Download 50c53f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-28T00:46:39+01:00 Download 8e57676
Download 4f6292b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-27T23:10:41+01:00 Download 95075f2
Download b9aefe8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2022-12-10T11:52:39+01:00
Download 0cfdf42 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 6 2022-12-11T22:07:35+01:00
Download 8e57676 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2022-12-25T11:22:47+01:00
Download 7dc3f2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2022-12-10T01:17:40+01:00
Download 95075f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 12 2022-12-08T01:20:04+01:00

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

Trying to find witnesses for program (d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff, sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 20 witnesses for program sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c, d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fa16963 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T09:26:13+01:00
Download 130e0db Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2021-12-07T09:30:39Z
Download a0148ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 6 2021-12-05T18:34:39+01:00
Download 8c7c4b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 6 2021-12-08T18:28:20+01:00
Download a414cd3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 6 2021-12-09T13:09:30+01:00
Download ca7d512 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 11 2021-12-09T23:14:24Z
Download 79110a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 10 2021-12-06T16:10:44Z
Download 6872721 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness 2LS 14 2021-12-05T20:44:22+01:00
Download 8bf990b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness SESL 2 2021-12-06T12:17:37+01:00
Download 0781ac4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.8 3 2021-12-13T20:23:42Z
Download aabdb2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2021-12-10T21:06:38+01:00 Download cd2bb1a
Download 578d2b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2021-12-09T15:42:49+01:00 Download 0c99d4c
Download bcfa3d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2021-12-08T22:13:51+01:00 Download 9c63158
Download 02e9d3e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2021-12-06T01:16:12+01:00 Download d9903ab
Download 350e024 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2021-12-05T20:12:50+01:00 Download fc12bc0
Download fc12bc0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2021-12-05T18:03:34+01:00
Download cd2bb1a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 6 2021-12-10T19:16:36+01:00
Download 9c63158 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 6 2021-12-08T19:38:05+01:00
Download 0c99d4c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 6 2021-12-09T12:09:56+01:00
Download d9903ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 12 2021-12-05T23:43:59+01:00

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

Trying to find witnesses for program (d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff, sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 10 witnesses for program sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c, d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 54c0513 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T17:52:30+01:00
Download d0cef91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 6 2020-12-05T17:15:33+01:00
Download 2b5288c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 6 2020-12-08T05:30:50+01:00
Download 811ffcd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.1 3 2020-12-06T23:51:14
Download 6a33b1d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) unknown_witness Goblint (svcomp21-0-g82e03b87) 3 2020-12-07T17:12:16
Download 8c3ac83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 6 2020-12-08T07:43:52+01:00 Download 7c97fb9
Download beb36a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 6 2020-12-06T16:43:18+01:00 Download 17ff137
Download 78cc1d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 6 2020-12-06T13:43:10+01:00 Download d044548
Download d044548 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 6 2020-12-05T16:57:44+01:00
Download 7c97fb9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 6 2020-12-08T04:04:31+01:00

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

Trying to find witnesses for program (d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff, sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2606f07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 6 2019-11-30T15:00:56+01:00
Download f013d3d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 6 2019-12-01T02:36:04+01:00
Download 0a435b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 6 2019-11-30T04:03:18+01:00
Download a40902c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 6 2019-11-30T21:10:09+01:00

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

Trying to find witnesses for program (d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff, sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 2 witnesses for program sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c, d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 147876d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-07T12:26:40+01:00
Download eb1d1e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T00:48:14+01:00

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

Trying to find witnesses for program (d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff, sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 4 witnesses for program sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c, d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a55a5ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T18:44:03.052416
Download 5f73e09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T11:10:00+01:00
Download 8dab248 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 11 2017-12-01T10:22 CET (sv-comp)
Download 5d96b0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 7 2017-12-01T19:00 CET (sv-comp)

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

Trying to find witnesses for program (d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff, sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c).

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

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