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/loop-acceleration/diamond_true-unreach-call1_true-termination.i
programSHA ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e
witnessName results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-reachsafety.diamond_true-unreach-call1_true-termination.i.files/witness.graphml
witnessSHA 447ee4ab162399bb9b2817c177dc4ec2a5a30cb5b3119fa9189515feb048012c

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-05T10:23:36.321868
producer DepthK v3.0
programfile /tmp/vcloud-vcloud-master/worker/working_dir_75817f3d-7e69-41bc-90af-20ee27ad26b3/sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call1_true-termination.i
programhash 34d122a13bd58fefb9ce641bf4f698a50b680c32
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/447ee4ab162399bb9b2817c177dc4ec2a5a30cb5b3119fa9189515feb048012c.graphml
witness-sha256 447ee4ab162399bb9b2817c177dc4ec2a5a30cb5b3119fa9189515feb048012c
witness-size 3488
witness-type correctness_witness

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

Trying to find witnesses for program (ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e, sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call1_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call1_true-termination.i, ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e.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 '23

Trying to find witnesses for program (ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e, sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call1_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call1_true-termination.i, ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e.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 '22

Trying to find witnesses for program (ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e, sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call1_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call1_true-termination.i, ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e.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 '21

Trying to find witnesses for program (ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e, sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call1_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call1_true-termination.i, ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e.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 (ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e, sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call1_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call1_true-termination.i, ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e.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 (ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e, sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call1_true-termination.i).

Found 20 witnesses for program sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call1_true-termination.i, ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0c83552 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T04:24 CET (sv-comp)
Download 10d9b46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T04:18:13
Download 7218c8f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T15:13 CET (sv-comp)
Download b19f687 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 6 2018-12-10T17:53:32+01:00
Download 973a7f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 8 2018-12-07T20:34:53+01:00
Download b74436b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-10T20:14:29+01:00 Download b19f687
Download 3c562fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T21:06:45+01:00 Download 404368c
Download 50a0fea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T23:07:40+01:00 Download 0c83552
Download c471856 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T21:42:00+01:00 Download 10d9b46
Download 6a7afdc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T06:21:46+01:00 Download 973a7f4
Download 65fa496 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T04:08:22+01:00 Download b9d170d
Download d4e6eef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T03:07:24+01:00 Download dae7567
Download 4dd3eef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T16:39:31+01:00 Download 7218c8f
Download 8b32c1d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:29:02+01:00 Download 447ee4a
Download 35996e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:00:48+01:00 Download 325aaa6
Download c56b695 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:08:03+01:00 Download 6a9dad9
Download 8bc1d88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:02:28+01:00 Download 489e001
Download 325aaa6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-05T10:06:27+01:00
Download 54abe73 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T17:51 CET (sv-comp)
Download d63b7ba Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T01:19 CET (sv-comp)

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

Trying to find witnesses for program (ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e, sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call1_true-termination.i).

Found 25 witnesses for program sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call1_true-termination.i, ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d1402fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T08:32 CET (sv-comp)
Download 36618d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 3 2017-12-01T20:38 CET (sv-comp)
Download 0abb961 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T00:38:55.374093
Download e0a2e20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T13:26:06.439178
Download 7f60b0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T13:43:18.059839
Download 0a47a1d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T14:09:14.545479
Download 0928426 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 82 2017-12-01T19:27 CET (sv-comp)
Download 49d130c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 7 2017-12-03T02:17:19+01:00
Download 968a0fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T07:34:55+01:00
Download 950c55a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T04:21:58+01:00 dc57dc6
Download 81d9fce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T20:54:07+01:00 7959513
Download 2166bb2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T14:26:47+01:00 67cfcae
Download 9e382f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T08:42:07+01:00 1da9545
Download 18eb45e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T22:34:25+01:00 66eaf8d
Download b48b796 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T22:18:52+01:00 9320996
Download 712212f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T08:13:57+01:00 c33ee95
Download 25a228c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T06:55:23+01:00 07a2400
Download 8b20c49 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T06:45:18+01:00 897a54b
Download 0be899d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T04:41:57+01:00 4261bcc
Download 442c6c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-11-30T11:57:04+01:00
Download fa60184 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 6 2017-12-02T06:14:27+01:00
Download df219bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 236 2017-11-30T15:37 CET (sv-comp)
Download c8ad605 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 103 2017-11-30T17:45 CET (sv-comp)
Download b6f8113 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 236 2017-12-01T13:46 CET (sv-comp)
Download 0f8a49a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2017-12-01T12:38 CET (sv-comp)

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

Trying to find witnesses for program (ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e, sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call1_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loop-acceleration/diamond_true-unreach-call1_true-termination.i, ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ee56f280085f50ab3972d0d0dd074ceecc53d3fcd48e44d50a1ac06e0f4bd25e.json

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