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/floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i
programSHA 0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353
witnessName results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.newton_1_7_false-unreach-call_true-termination.i.files/witness.graphml
witnessSHA 08614a4913f2ab0c9f0e666391a0f614881ae70c13eca064a59bc704eea1a9ca

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/08614a4913f2ab0c9f0e666391a0f614881ae70c13eca064a59bc704eea1a9ca.json

Key Value
architecture 32bit
creationtime 2017-11-30T19:59:21+01:00
producer CPAchecker 1.6.1-svn 26773
program-sha256 0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353
programfile ../../sv-benchmarks/c/floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i
programhash 70fe3c899c400d059184c32a286d7d2375d5f495
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/08614a4913f2ab0c9f0e666391a0f614881ae70c13eca064a59bc704eea1a9ca.graphml
witness-sha256 08614a4913f2ab0c9f0e666391a0f614881ae70c13eca064a59bc704eea1a9ca
witness-size 5802
witness-type violation_witness

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

Trying to find witnesses for program (0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353, sv-benchmarks/c/floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i, 0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353.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 (0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353, sv-benchmarks/c/floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i, 0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353.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 (0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353, sv-benchmarks/c/floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i, 0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353.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 (0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353, sv-benchmarks/c/floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i, 0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353.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 (0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353, sv-benchmarks/c/floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i).

Found 19 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i, 0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 78309c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 5 2019-12-04T00:31 CET (comp)
Download de21e76 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T21:48:30+01:00 Download 068f19d
Download c29bd3a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T01:52:05+01:00 Download c22f41e
Download fafa220 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T00:27:12+01:00 Download f69b963
Download 4afa57a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T21:15:47+01:00 Download 35bde33
Download 90cd74f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T20:20:35+01:00 Download 1c9602e
Download 22bc1a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T19:34:09+01:00 Download 60cc553
Download 2e653e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-04T02:58:33+01:00 Download 78309c6
Download 2d499b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-03T08:58:12+01:00 Download 7116c9d
Download f8ab023 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-03T08:09:49+01:00 Download f90f6a5
Download f90f6a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 6 2019-11-29T19:03:56+01:00
Download c22f41e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 4 2019-12-07T20:43:23+01:00
Download 068f19d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 5 2019-12-01T06:05:34+01:00
Download f7d3496 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness BRICK 3 2019-12-07T21:37:18Z
Download 51500d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T21:09:25+01:00 Download a0e2e26
Download 7191acb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:54:23+01:00 Download e1e5388
Download 0a4d28c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:44:40+01:00 Download 1466b08
Download 4cc9cae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T23:51:26+01:00 Download f7d3496
Download 1ca996b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:16 CET (comp)

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

Trying to find witnesses for program (0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353, sv-benchmarks/c/floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i).

Found 17 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i, 0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3bd2aad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 5 2018-12-07T06:57 CET (sv-comp)
Download fe0dc5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 5 2018-12-10T18:58:47+01:00
Download 99aa15e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-06T22:49:02+01:00
Download 101bf61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-10T20:37:34+01:00 Download fe0dc5b
Download d941fda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:53:28+01:00 Download 428e2c8
Download 78cf0bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:38:45+01:00 Download d04c65d
Download 67b027c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T18:20:34+01:00 Download c128cd0
Download 4756ad3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T07:44:58+01:00 Download 99aa15e
Download b7e47f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T04:58:21+01:00 Download 19ed824
Download cb8c85e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-07T17:45:36+01:00 Download 3bd2aad
Download f7ac713 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T10:17:14+01:00 Download dfd38d8
Download 5bc82e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:48:44+01:00 Download 207b1be
Download 9e6f5cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:40:48+01:00 Download 15b52b0
Download e687b69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:19:51+01:00 Download c7407e6
Download d6d5f06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:18:36+01:00 Download 026f90e
Download 207b1be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T05:26:28+01:00
Download 18e4b97 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T05:18 CET (sv-comp)

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

Trying to find witnesses for program (0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353, sv-benchmarks/c/floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i).

Found 16 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i, 0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download bf6f01c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T22:21 CET (sv-comp)
Download 513fbfc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 6 2017-12-03T04:57Z
Download 3473fe7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T17:08:15.285952
Download b142fc4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T10:23:13.772947
Download 6ea9e48 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 6 2017-12-02T20:05:34+01:00
Download 08614a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-11-30T19:59:21+01:00
Download 47ec6b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 13 2017-11-30T14:15:32+01:00
Download b343239 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 6 2017-11-30T21:14:20+01:00
Download 7efa03a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 7 2017-12-02T01:17:05+01:00
Download c58ac7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 4 2017-12-01T02:25 CET (sv-comp)
Download 8e8ca8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 6 2017-12-02T17:58Z
Download 762d536 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 4 2017-11-30T20:30 CET (sv-comp)
Download c6ec210 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T23:50:02.166768
Download a7e9e5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T12:19:58.432696
Download dfbb926 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 5 2017-12-01T13:55 CET (sv-comp)
Download 244ad8c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 10 2017-12-01T17:14 CET (sv-comp)

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

Trying to find witnesses for program (0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353, sv-benchmarks/c/floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i, 0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/0b2f165068f63c3324577478d008dfe4820e56f99e912142662d5825ef30f353.json

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