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 (13e06838d3810c8c8097ed313b9b8b744669757fc6cbd24675d296c6a57d83ed, sv-benchmarks/c/floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i).

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

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

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

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

Found 12 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i, 13e06838d3810c8c8097ed313b9b8b744669757fc6cbd24675d296c6a57d83ed
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/13e06838d3810c8c8097ed313b9b8b744669757fc6cbd24675d296c6a57d83ed.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b0e3f7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T22:56 CET (comp)
Download 9a0b44a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:17:54+01:00 Download 9769a26
Download 04283cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:02:32+01:00 Download 4ca85c6
Download 466c0b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T00:36:31+01:00 Download 69668f8
Download fe30307 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T23:46:44+01:00 Download 43e9f70
Download 4fbf74b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T19:03:00+01:00 Download f70db4d
Download d4337a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-04T02:13:02+01:00 Download b0e3f7a
Download 64b04d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-11-30T16:55:02+01:00 Download 46174c0
Download 46174c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 6 2019-11-29T20:25:44+01:00
Download 69668f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 6 2019-12-07T13:16:59+01:00
Download 43e9f70 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness BRICK 3 2019-12-07T21:38:55Z
Download 60889c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:54 CET (comp)

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

Trying to find witnesses for program (13e06838d3810c8c8097ed313b9b8b744669757fc6cbd24675d296c6a57d83ed, sv-benchmarks/c/floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i).

Found 14 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i, 13e06838d3810c8c8097ed313b9b8b744669757fc6cbd24675d296c6a57d83ed
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/13e06838d3810c8c8097ed313b9b8b744669757fc6cbd24675d296c6a57d83ed.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fd1b6f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T06:16 CET (sv-comp)
Download 4ec4295 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 6 2018-12-10T17:53:15+01:00
Download b9d1035 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-07T09:30:30+01:00
Download d9b7174 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-10T20:28:25+01:00 Download 4ec4295
Download 0eb4bbe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T05:51:29+01:00 Download b9d1035
Download 723b6db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T04:41:47+01:00 Download c0ee223
Download 4814346 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T16:52:47+01:00 Download fd1b6f4
Download 61a305d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:43:33+01:00 Download eaa12df
Download d7596bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:09:05+01:00 Download 361d87d
Download cdbe2d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:36:23+01:00 Download d71f541
Download 17efde2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:15:29+01:00 Download e637f89
Download c178a10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T07:39:58+01:00 Download 299389c
Download 361d87d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-05T11:16:40+01:00
Download 06de83c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T06:42 CET (sv-comp)

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

Trying to find witnesses for program (13e06838d3810c8c8097ed313b9b8b744669757fc6cbd24675d296c6a57d83ed, sv-benchmarks/c/floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i).

Found 14 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i, 13e06838d3810c8c8097ed313b9b8b744669757fc6cbd24675d296c6a57d83ed
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/13e06838d3810c8c8097ed313b9b8b744669757fc6cbd24675d296c6a57d83ed.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 42a2e25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 7 2017-12-01T01:34:54+01:00
Download 722b4f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 8 2017-12-02T09:41:04+01:00
Download 8123a92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T20:39:15.749185
Download 9b30ac6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T09:48:31.057165
Download 4828100 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T16:34:09.270401
Download bef51ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T08:31:08.147028
Download 2ba9e66 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-02T09:14:02+01:00 90b0266
Download d6d0386 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T22:42:31+01:00 d37d53e
Download d750add Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T06:18:19+01:00 dc20fa8
Download 998e27c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T05:47:26+01:00 62f96f8
Download 3da3c13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 6 2017-11-30T16:35 CET (sv-comp)
Download b9a93f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 15 2017-11-30T15:58 CET (sv-comp)
Download 748d755 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 6 2017-12-01T15:28 CET (sv-comp)
Download ac26195 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 15 2017-12-01T13:40 CET (sv-comp)

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

Trying to find witnesses for program (13e06838d3810c8c8097ed313b9b8b744669757fc6cbd24675d296c6a57d83ed, sv-benchmarks/c/floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i).

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

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