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_2_8_false-unreach-call_true-termination.i
programSHA 3b2d2cf2875c43cc813d8bdd0bfb82864e79ab8d7db276f34207cc91d5ecc640
witnessName results-verified/utaipan.2018-12-08_1419.logfiles/sv-comp19_prop-reachsafety.newton_2_8_false-unreach-call_true-termination.i.files/witness.graphml
witnessSHA c1566f95eeb1674231f0463d35ce5b081a5907c7c5c063de2f215c607e7f0dcb

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-08T18:11Z
producer Taipan
programfile /tmp/vcloud-vcloud-master/worker/working_dir_1dab5451-4d6d-41f3-a0df-a81d44c681f1/sv-benchmarks/c/floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i
programhash 2d89a0564bbb0fd26a33f9c676f8f302637a0505
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/c1566f95eeb1674231f0463d35ce5b081a5907c7c5c063de2f215c607e7f0dcb.graphml
witness-sha256 c1566f95eeb1674231f0463d35ce5b081a5907c7c5c063de2f215c607e7f0dcb
witness-size 8670
witness-type violation_witness

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

Trying to find witnesses for program (3b2d2cf2875c43cc813d8bdd0bfb82864e79ab8d7db276f34207cc91d5ecc640, sv-benchmarks/c/floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i).

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

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

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

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

Found 18 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i, 3b2d2cf2875c43cc813d8bdd0bfb82864e79ab8d7db276f34207cc91d5ecc640
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/3b2d2cf2875c43cc813d8bdd0bfb82864e79ab8d7db276f34207cc91d5ecc640.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6c73105 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 6 2019-12-04T00:08 CET (comp)
Download 55a35d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-11T21:59:31+01:00 Download 8d38e95
Download f6d38db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-08T01:58:51+01:00 Download 7cf12c9
Download 921021a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-08T00:27:20+01:00 Download 4028a58
Download 31a11e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-07T21:18:02+01:00 Download b157157
Download a30a849 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-04T02:58:41+01:00 Download 6c73105
Download 816b1f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-03T08:10:48+01:00 Download d1dbffa
Download d1dbffa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 8 2019-11-29T15:35:23+01:00
Download 7cf12c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 5 2019-12-07T12:36:24+01:00
Download 8d38e95 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 8 2019-12-01T03:07:01+01:00
Download 5923963 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness BRICK 4 2019-12-07T21:36:15Z
Download e7cc997 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T21:09:38+01:00 Download 42eb419
Download 804260c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:54:26+01:00 Download 26c79e4
Download c6c34f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:44:39+01:00 Download 6f2d973
Download c91e60b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T23:51:15+01:00 Download 5923963
Download 7e923c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T20:20:27+01:00 Download 065c809
Download eab4556 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T19:34:19+01:00 Download e275582
Download 11ed8fe Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T01:01 CET (comp)

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

Trying to find witnesses for program (3b2d2cf2875c43cc813d8bdd0bfb82864e79ab8d7db276f34207cc91d5ecc640, sv-benchmarks/c/floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b969d0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 6 2018-12-07T01:59 CET (sv-comp)
Download 8cc3d86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 6 2018-12-10T17:09:03+01:00
Download d5037f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-06T21:26:31+01:00
Download 0dcaad2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-10T20:38:23+01:00 Download 8cc3d86
Download 3343f0d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T20:53:27+01:00 Download c1566f9
Download 9b8a583 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T20:39:11+01:00 Download 5930a98
Download 426f734 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T18:21:45+01:00 Download f7e5c38
Download d442e1e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T08:48:50+01:00 Download d5037f3
Download 22a955f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-07T17:45:51+01:00 Download b969d0a
Download adee01c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:48:23+01:00 Download e6ba221
Download 10f76f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:40:48+01:00 Download afba1f6
Download 324c47a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:18:21+01:00 Download 386909a
Download e6ba221 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-05T23:07:08+01:00
Download ffc051b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T05:03:46+01:00 Download a1108c0
Download 14d167c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T10:18:16+01:00 Download 4f26b10
Download 84722d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:19:37+01:00 Download f711675
Download 5518fd0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T04:12 CET (sv-comp)

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

Trying to find witnesses for program (3b2d2cf2875c43cc813d8bdd0bfb82864e79ab8d7db276f34207cc91d5ecc640, sv-benchmarks/c/floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i).

Found 15 witnesses for program sv-benchmarks/c/floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i, 3b2d2cf2875c43cc813d8bdd0bfb82864e79ab8d7db276f34207cc91d5ecc640
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/3b2d2cf2875c43cc813d8bdd0bfb82864e79ab8d7db276f34207cc91d5ecc640.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6de37b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T22:22 CET (sv-comp)
Download da20030 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 8 2017-12-02T21:41Z
Download 6508a40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T00:06:01.044999
Download ab0fc46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T18:00:46.650924
Download 1941e1a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 7 2017-11-30T16:37:13+01:00
Download 817b5f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 18 2017-11-30T17:18:02+01:00
Download 9b297e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 7 2017-12-01T02:34:25+01:00
Download 755d071 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 8 2017-12-02T01:12:12+01:00
Download a5d3249 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 4 2017-11-30T18:22 CET (sv-comp)
Download 7423b75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 8 2017-12-02T09:30Z
Download 2f0d2a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 4 2017-12-01T01:17 CET (sv-comp)
Download 191f756 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T20:30:57.209767
Download 39aac3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T11:49:48.614835
Download 4ad80b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 6 2017-12-01T18:52 CET (sv-comp)
Download 0c4169c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 15 2017-12-01T13:50 CET (sv-comp)

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

Trying to find witnesses for program (3b2d2cf2875c43cc813d8bdd0bfb82864e79ab8d7db276f34207cc91d5ecc640, sv-benchmarks/c/floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i).

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

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