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-cbmc-regression/float-no-simp4_true-unreach-call.i
programSHA 7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b
witnessName results-verified/cbmc.2018-12-04_2248.logfiles/sv-comp19_prop-reachsafety.float-no-simp4_true-unreach-call.i.files/witness.graphml
witnessSHA b16995faa804d2c1fa575d3aa1ee66d750d722b4152ba910abaa3ec6eabe8557

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-05T02:29 CET (sv-comp)
producer CBMC
programfile ../../sv-benchmarks/c/floats-cbmc-regression/float-no-simp4_true-unreach-call.i
programhash 356e353e7bb6e96bd959fe4862b56669bada9c19
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/b16995faa804d2c1fa575d3aa1ee66d750d722b4152ba910abaa3ec6eabe8557.graphml
witness-sha256 b16995faa804d2c1fa575d3aa1ee66d750d722b4152ba910abaa3ec6eabe8557
witness-size 22906
witness-type correctness_witness

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

Trying to find witnesses for program (7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b, sv-benchmarks/c/floats-cbmc-regression/float-no-simp4_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float-no-simp4_true-unreach-call.i, 7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b.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 (7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b, sv-benchmarks/c/floats-cbmc-regression/float-no-simp4_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float-no-simp4_true-unreach-call.i, 7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b.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 (7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b, sv-benchmarks/c/floats-cbmc-regression/float-no-simp4_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float-no-simp4_true-unreach-call.i, 7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b.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 (7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b, sv-benchmarks/c/floats-cbmc-regression/float-no-simp4_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float-no-simp4_true-unreach-call.i, 7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b.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 (7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b, sv-benchmarks/c/floats-cbmc-regression/float-no-simp4_true-unreach-call.i).

Found 16 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float-no-simp4_true-unreach-call.i, 7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a4aa9ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T23:25 CET (comp)
Download 244da5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-11T20:29:08+01:00 Download 0d264ca
Download 5bff790 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-11T20:08:20+01:00 Download ea6f4f3
Download aba3386 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-11T20:02:17+01:00 Download f39c499
Download d1c7aae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-08T00:36:56+01:00 Download 1095b10
Download dc650b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-07T23:47:54+01:00 Download cea2fa7
Download 8b16dc3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-07T23:44:37+01:00 Download 268cb46
Download a15a38f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-07T19:44:59+01:00 Download d4fc70c
Download 49c218b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-05T19:12:57+01:00 Download 994603a
Download 671ebee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-05T19:02:54+01:00 Download d7b0057
Download aed102f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-12-04T02:07:31+01:00 Download a4aa9ec
Download d33c7ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 8 2019-11-30T16:45:00+01:00 Download 70cd691
Download 70cd691 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 8 2019-11-30T14:43:59+01:00
Download 1095b10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 8 2019-12-07T21:50:54+01:00
Download ea6f4f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 8 2019-11-30T21:26:00+01:00
Download cea2fa7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness BRICK 3 2019-12-07T21:35:54Z

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

Trying to find witnesses for program (7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b, sv-benchmarks/c/floats-cbmc-regression/float-no-simp4_true-unreach-call.i).

Found 16 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float-no-simp4_true-unreach-call.i, 7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 114901f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-07T20:26:53
Download 4825427 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T10:47 CET (sv-comp)
Download dd5fb39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 8 2018-12-10T19:12:15+01:00
Download 0f6a61d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-10T19:41:27+01:00 Download dd5fb39
Download 738c19a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-09T20:14:43+01:00 Download cc9fcfa
Download 0b4f9d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-09T17:36:55+01:00 Download 349e1a9
Download 299aced Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-08T21:34:13+01:00 Download 114901f
Download 1af6c54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-08T03:17:40+01:00 Download 9418274
Download 7672167 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-07T17:43:02+01:00 Download 1cfbd9f
Download f67f5e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-07T16:38:43+01:00 Download 4825427
Download 16470f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:28:36+01:00 Download 34566f7
Download b587a2b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:14:31+01:00 Download e210f92
Download 2742303 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T08:22:22+01:00 Download c92ee33
Download 911cf96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T08:18:53+01:00 Download b16995f
Download d33c31c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T08:02:32+01:00 Download ad93360
Download e210f92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-05T11:59:44+01:00

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

Trying to find witnesses for program (7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b, sv-benchmarks/c/floats-cbmc-regression/float-no-simp4_true-unreach-call.i).

Found 21 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float-no-simp4_true-unreach-call.i, 7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1c491b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 7 2017-11-30T18:54:08+01:00
Download 3011c91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 55 2017-12-03T00:10Z
Download eaa1c73 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 59 2017-12-02T14:44Z
Download b99a281 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T17:26:03.724770
Download ef22fd8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T08:48:47.683700
Download 631cfe2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 12 2017-12-02T23:43:09+01:00
Download 730cdca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T07:00:16+01:00
Download c579681 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 12 2017-12-03T06:52:01+01:00 c429ecc
Download 2b3acb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 12 2017-12-03T04:23:32+01:00 9ca0429
Download 7d6418b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 12 2017-12-03T01:49:15+01:00 8293c6f
Download 7252a1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 12 2017-12-03T01:21:17+01:00 66a216f
Download 28cdc0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 12 2017-12-02T08:26:45+01:00 bbbced9
Download 7a221a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 12 2017-12-01T22:24:28+01:00 6c9466d
Download b7edfa5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 12 2017-12-01T08:13:10+01:00 3ed694f
Download ee400b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 12 2017-12-01T07:10:58+01:00 65d5982
Download 0372008 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 12 2017-12-01T07:03:31+01:00 2334a83
Download e59ac6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 12 2017-12-01T05:50:53+01:00 5b9428d
Download f25d757 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 12 2017-11-30T19:05:33+01:00
Download fda46e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 23 2017-11-30T14:43 CET (sv-comp)
Download 7a8471f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 55 2017-12-02T00:32Z
Download d83585f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 168 2017-11-30T17:44 CET (sv-comp)

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

Trying to find witnesses for program (7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b, sv-benchmarks/c/floats-cbmc-regression/float-no-simp4_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float-no-simp4_true-unreach-call.i, 7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/7a7a9c8775353e8095f364a05ed18dcdc980146cb2118a6420d6a43d2c4d328b.json

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