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_5_false-unreach-call_true-termination.i
programSHA 5fe3f54f34f5155da87e27d79a5a2b03fa0cbae9f8bcf9ad7f258a15fa706c85
witnessName results-validated/cpa-seq-validate-violation-witnesses-pesco.2018-12-08_0739.logfiles/sv-comp19_prop-reachsafety.newton_1_5_false-unreach-call_true-termination.i.files/witness.graphml
witnessSHA e66acc8a222819863cccfbee09989996bc0d36c0ba626a160bb9d520abfc5328

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-08T07:46:27+01:00
inputwitnesshash 198656fb81f65280ac2ebbd54e160edb8b3309a41253a698c8080f6baff1109c
producer CPAchecker 1.7-svn 29852
program-sha256 5fe3f54f34f5155da87e27d79a5a2b03fa0cbae9f8bcf9ad7f258a15fa706c85
programfile ../../sv-benchmarks/c/floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i
programhash 5fe3f54f34f5155da87e27d79a5a2b03fa0cbae9f8bcf9ad7f258a15fa706c85
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/e66acc8a222819863cccfbee09989996bc0d36c0ba626a160bb9d520abfc5328.graphml
witness-sha256 e66acc8a222819863cccfbee09989996bc0d36c0ba626a160bb9d520abfc5328
witness-size 6421
witness-type violation_witness

This witness was created for this program (cf. table above, 5fe3f54f34f5155da87e27d79a5a2b03fa0cbae9f8bcf9ad7f258a15fa706c85).

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

Trying to find witnesses for program (5fe3f54f34f5155da87e27d79a5a2b03fa0cbae9f8bcf9ad7f258a15fa706c85, sv-benchmarks/c/floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i).

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8327124 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 5 2019-12-04T00:21 CET (comp)
Download 8cc955d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T21:43:25+01:00 Download 33a8109
Download 94398e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T01:53:32+01:00 Download be6c163
Download 00e4f1f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T21:15:44+01:00 Download f255892
Download 70c065f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T20:20:36+01:00 Download f4cec28
Download aa0d1b9 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 00993a1
Download be38914 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-04T02:58:43+01:00 Download 8327124
Download afe487a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-03T08:58:33+01:00 Download a4ba383
Download 94b1b26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-03T08:09:05+01:00 Download 7ed6edd
Download 7ed6edd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 6 2019-11-30T09:44:01+01:00
Download be6c163 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 4 2019-12-07T15:42:02+01:00
Download 33a8109 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 5 2019-12-01T11:40:05+01:00
Download 435a71c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness BRICK 3 2019-12-07T21:36:37Z
Download ee40f0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T21:09:09+01:00 Download 2837f96
Download 2a70f72 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:54:48+01:00 Download a1b58af
Download a61434a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:44:38+01:00 Download 3ac037b
Download a17df29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T00:27:31+01:00 Download 361b683
Download 2385828 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T23:51:13+01:00 Download 435a71c
Download 8b30520 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:20 CET (comp)

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

Trying to find witnesses for program (5fe3f54f34f5155da87e27d79a5a2b03fa0cbae9f8bcf9ad7f258a15fa706c85, sv-benchmarks/c/floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4d6ac83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 5 2018-12-07T06:31 CET (sv-comp)
Download 69515b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 5 2018-12-10T18:29:59+01:00
Download 198656f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T21:10:21+01:00
Download 3841f25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-10T20:37:18+01:00 Download 69515b8
Download ca8ff00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:53:29+01:00 Download 6ce1746
Download 0a4e42b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:35:43+01:00 Download e916a2a
Download e868fc6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T18:21:06+01:00 Download 4932f42
Download e66acc8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T07:46:27+01:00 Download 198656f
Download 35366e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T04:51:47+01:00 Download dca7007
Download 4208341 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-07T17:45:10+01:00 Download 4d6ac83
Download 8f9bc94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T10:20:16+01:00 Download 3ea8130
Download c1cf4be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:48:22+01:00 Download 96fa882
Download c64cc44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:42:28+01:00 Download c5c5fec
Download 6156207 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:20:28+01:00 Download a4ddfa0
Download 1d0838b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:14:14+01:00 Download bc244a9
Download 96fa882 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-05T20:34:46+01:00
Download b796b38 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T09:09 CET (sv-comp)

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

Trying to find witnesses for program (5fe3f54f34f5155da87e27d79a5a2b03fa0cbae9f8bcf9ad7f258a15fa706c85, sv-benchmarks/c/floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 26ee070 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T23:28 CET (sv-comp)
Download ea5b03a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 6 2017-12-02T21:53Z
Download 5a20965 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T15:38:44.113796
Download ac5c94c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T09:50:44.639880
Download bb298fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 6 2017-12-03T02:25:41+01:00
Download 5b01413 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-11-30T18:01:34+01:00
Download bd1ecae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 13 2017-11-30T14:07:39+01:00
Download 54ba007 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 6 2017-11-30T13:02:34+01:00
Download bc30879 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 7 2017-12-01T22:39:01+01:00
Download 35e3589 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 4 2017-11-30T16:38 CET (sv-comp)
Download aeb3ddb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 6 2017-12-02T20:50Z
Download b92cb65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 4 2017-11-30T22:51 CET (sv-comp)
Download f8afc48 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T02:03:09.141877
Download c145467 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T13:13:01.623620
Download c66e1d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 5 2017-12-01T14:59 CET (sv-comp)
Download 04cc7ec Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 10 2017-12-01T14:49 CET (sv-comp)

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

Trying to find witnesses for program (5fe3f54f34f5155da87e27d79a5a2b03fa0cbae9f8bcf9ad7f258a15fa706c85, sv-benchmarks/c/floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i).

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

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