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/float20_true-unreach-call_true-termination.i
programSHA 8851ede3244374d30ca55331f8e365202e10bee229701230c1e194cb0d2bb493
witnessName results-verified/cbmc.2018-12-04_2248.logfiles/sv-comp19_prop-reachsafety.float20_true-unreach-call_true-termination.i.files/witness.graphml
witnessSHA cb2be26fa9a2f6c558bbf794cbf1c0362a29e5293ca2d8b5d535be5c32e05b82

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-05T05:42 CET (sv-comp)
producer CBMC
programfile ../../sv-benchmarks/c/floats-cbmc-regression/float20_true-unreach-call_true-termination.i
programhash 0141f30eebc41972a05a5b9a00ccec3818dc94e8
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/cb2be26fa9a2f6c558bbf794cbf1c0362a29e5293ca2d8b5d535be5c32e05b82.graphml
witness-sha256 cb2be26fa9a2f6c558bbf794cbf1c0362a29e5293ca2d8b5d535be5c32e05b82
witness-size 8831
witness-type correctness_witness

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

Trying to find witnesses for program (8851ede3244374d30ca55331f8e365202e10bee229701230c1e194cb0d2bb493, sv-benchmarks/c/floats-cbmc-regression/float20_true-unreach-call_true-termination.i).

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

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

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

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

Found 19 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float20_true-unreach-call_true-termination.i, 8851ede3244374d30ca55331f8e365202e10bee229701230c1e194cb0d2bb493
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/8851ede3244374d30ca55331f8e365202e10bee229701230c1e194cb0d2bb493.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0a2b660 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T23:16 CET (comp)
Download 8c7c9eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-11T20:13:57+01:00 Download 378d0fb
Download 65f424e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-11T20:07:26+01:00 Download 094ca78
Download 019dea5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-11T20:03:00+01:00 Download f9a7da1
Download b87fb22 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-08T00:37:00+01:00 Download 4a1dfdb
Download d709036 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-07T23:47:07+01:00 Download faf40c2
Download 0228bd0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-07T23:29:20+01:00 Download 25cdade
Download 6cdde0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-07T19:47:37+01:00 Download e5d7e3a
Download 7f48c8f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-05T19:13:15+01:00 Download cff0d19
Download f3c86c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-05T19:02:49+01:00 Download c4738b7
Download 29b806a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-04T02:07:50+01:00 Download 0a2b660
Download 8ee7233 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-11-30T19:47:58+01:00 Download 7733e3c
Download 5060f58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-11-30T16:14:44+01:00 Download 8ac03ec
Download 8ac03ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 6 2019-11-30T04:43:19+01:00
Download 4a1dfdb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 6 2019-12-07T14:55:33+01:00
Download 094ca78 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 6 2019-12-01T08:45:56+01:00
Download faf40c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness BRICK 3 2019-12-07T21:35:18Z
Download c88f4ef Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 1 2019-12-01 20:05:22
Download f7d2735 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:10 CET (comp)

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

Trying to find witnesses for program (8851ede3244374d30ca55331f8e365202e10bee229701230c1e194cb0d2bb493, sv-benchmarks/c/floats-cbmc-regression/float20_true-unreach-call_true-termination.i).

Found 19 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float20_true-unreach-call_true-termination.i, 8851ede3244374d30ca55331f8e365202e10bee229701230c1e194cb0d2bb493
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/8851ede3244374d30ca55331f8e365202e10bee229701230c1e194cb0d2bb493.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download eda72bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-07T23:05:08
Download 6922b82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-06T22:22 CET (sv-comp)
Download c8c3e5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-08T04:18:44+01:00
Download 20c7783 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-10T19:50:02+01:00 Download 2c6181b
Download e06687d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:27:04+01:00 Download e112fee
Download fc7d1a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:01:37+01:00 Download 031ed4f
Download ec4d20d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T19:53:18+01:00 Download c901f19
Download e687010 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-08T21:42:10+01:00 Download eda72bf
Download e6e8d86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-08T05:43:44+01:00 Download c8c3e5f
Download ccb39ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-08T03:23:05+01:00 Download c04a0e0
Download fc5b509 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-07T17:43:28+01:00 Download 9658555
Download 218d378 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-07T16:38:56+01:00 Download 6922b82
Download 8203de2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:28:39+01:00 Download 7cbcda8
Download 90b4db8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T08:45:25+01:00 Download cc55d70
Download 6563ca7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T08:17:04+01:00 Download cb2be26
Download 51c3017 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T07:45:01+01:00 Download 0c8b457
Download 8a5714f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T07:26:47+01:00 Download 7030252
Download cc55d70 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T07:18:42+01:00
Download 5401046 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T10:00 CET (sv-comp)

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

Trying to find witnesses for program (8851ede3244374d30ca55331f8e365202e10bee229701230c1e194cb0d2bb493, sv-benchmarks/c/floats-cbmc-regression/float20_true-unreach-call_true-termination.i).

Found 31 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float20_true-unreach-call_true-termination.i, 8851ede3244374d30ca55331f8e365202e10bee229701230c1e194cb0d2bb493
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/8851ede3244374d30ca55331f8e365202e10bee229701230c1e194cb0d2bb493.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 53dfdc9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T22:27 CET (sv-comp)
Download fa5111f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-02T02:40:00+01:00
Download 5605c89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 9 2017-12-02T23:28Z
Download 0d5c51a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 9 2017-12-02T09:42Z
Download 26d1b93 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T00:43:29.495117
Download 9876802 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T14:45:36.505498
Download 8103613 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T16:45:53.388147
Download fe51d85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T17:45:20.603756
Download e533a9e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 6 2017-12-01T21:44 CET (sv-comp)
Download 14091c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 8 2017-12-03T01:46:03+01:00
Download 4c50d5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-11-30T16:42:58+01:00
Download 4614197 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-03T06:58:58+01:00 b48d77b
Download 695e69d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-03T04:23:07+01:00 c5b6da9
Download 031f09a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-03T02:09:07+01:00 6918d05
Download 67b8224 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-03T01:42:50+01:00 f36247b
Download b510f8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-02T08:13:49+01:00 14a1d15
Download 399aa99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T22:30:11+01:00 b254a5b
Download acfbb98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T08:13:30+01:00 812ba02
Download 6d56cc6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T06:18:49+01:00 e4e3340
Download b7da7b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T05:58:24+01:00 d644bb6
Download c6114ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T05:13:28+01:00 f82cf07
Download fefe7db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T05:03:05+01:00 3750efa
Download 68180a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T04:55:38+01:00 e62bcca
Download 9bd05f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-11-30T18:07:06+01:00
Download e6c1800 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 15 2017-11-30T22:20:02+01:00
Download 1a48ad6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 8 2017-11-30T17:41:53+01:00
Download fc910ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 9 2017-11-30T20:03 CET (sv-comp)
Download a53d23d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 9 2017-12-02T06:57Z
Download 71b40a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 15 2017-11-30T11:48 CET (sv-comp)
Download be77eb6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 8 2017-12-01T15:22 CET (sv-comp)
Download fd745c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 15 2017-12-01T11:55 CET (sv-comp)

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

Trying to find witnesses for program (8851ede3244374d30ca55331f8e365202e10bee229701230c1e194cb0d2bb493, sv-benchmarks/c/floats-cbmc-regression/float20_true-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float20_true-unreach-call_true-termination.i, 8851ede3244374d30ca55331f8e365202e10bee229701230c1e194cb0d2bb493
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/8851ede3244374d30ca55331f8e365202e10bee229701230c1e194cb0d2bb493.json

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