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/float-benchs/float_double_true-unreach-call_true-termination.c
programSHA bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685
witnessName results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.float_double_true-unreach-call_true-termination.c.files/witness.graphml
witnessSHA 918ce8bc344c0476975cf3d8f8a74b2be92adda4c3f79cc0ae6fd6b5446b3dda

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/918ce8bc344c0476975cf3d8f8a74b2be92adda4c3f79cc0ae6fd6b5446b3dda.json

Key Value
architecture 32bit
creationtime 2017-11-30T20:21:35+01:00
producer CPAchecker 1.6.1-svn 26758M
program-sha256 bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685
programfile ../../sv-benchmarks/c/float-benchs/float_double_true-unreach-call_true-termination.c
programhash 773baadb55b498633b84884838d360efb3aec808
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/918ce8bc344c0476975cf3d8f8a74b2be92adda4c3f79cc0ae6fd6b5446b3dda.graphml
witness-sha256 918ce8bc344c0476975cf3d8f8a74b2be92adda4c3f79cc0ae6fd6b5446b3dda
witness-size 6787
witness-type correctness_witness

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

Trying to find witnesses for program (bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685, sv-benchmarks/c/float-benchs/float_double_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/float_double_true-unreach-call_true-termination.c, bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685.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 (bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685, sv-benchmarks/c/float-benchs/float_double_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/float_double_true-unreach-call_true-termination.c, bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685.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 (bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685, sv-benchmarks/c/float-benchs/float_double_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/float_double_true-unreach-call_true-termination.c, bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685.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 (bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685, sv-benchmarks/c/float-benchs/float_double_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/float_double_true-unreach-call_true-termination.c, bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685.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 (bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685, sv-benchmarks/c/float-benchs/float_double_true-unreach-call_true-termination.c).

Found 17 witnesses for program sv-benchmarks/c/float-benchs/float_double_true-unreach-call_true-termination.c, bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 9b192af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T22:41 CET (comp)
Download be2afd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:18:19+01:00 Download 1ba470d
Download 90d5c36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:15:14+01:00 Download 76bd178
Download 9370e00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:02:50+01:00 Download d473e2e
Download b10582e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-08T00:36:19+01:00 Download ff4c530
Download dc5d682 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:47:37+01:00 Download 93eb114
Download aaf68cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:39:28+01:00 Download 6aaee2b
Download 5f83a0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T19:44:45+01:00 Download bd12a3f
Download 2b742d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:12:46+01:00 Download 71d091f
Download 33a0e51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:03:05+01:00 Download 5280a4c
Download 290622f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-04T02:07:28+01:00 Download 9b192af
Download c7c48b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-11-30T19:53:51+01:00 Download a8eb642
Download 0ae5763 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-11-30T16:42:48+01:00 Download 8d2e4ba
Download 8d2e4ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 4 2019-11-30T10:00:59+01:00
Download ff4c530 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 4 2019-12-07T22:29:04+01:00
Download 1ba470d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 4 2019-12-01T05:59:12+01:00
Download 93eb114 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness BRICK 3 2019-12-07T21:37:13Z

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

Trying to find witnesses for program (bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685, sv-benchmarks/c/float-benchs/float_double_true-unreach-call_true-termination.c).

Found 21 witnesses for program sv-benchmarks/c/float-benchs/float_double_true-unreach-call_true-termination.c, bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 87996a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T17:56 CET (sv-comp)
Download 080e1fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T09:34:38
Download 5ebe149 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T02:48 CET (sv-comp)
Download d67274a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-07T04:09:27+01:00
Download 5200862 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-10T19:51:23+01:00 Download 3c4fb80
Download f2e1c2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-10T10:30:49+01:00 Download 8a446d5
Download 1c74988 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:25:57+01:00 Download 859db52
Download 283c7cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T19:52:12+01:00 Download ca13465
Download 461ee98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T17:28:39+01:00 Download 6c072be
Download a6ed4c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T23:08:01+01:00 Download 87996a2
Download 33b74a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T21:32:13+01:00 Download 080e1fb
Download caa944b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T05:44:43+01:00 Download d67274a
Download e8f1df5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T04:26:03+01:00 Download 1ef1d27
Download da3f1af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T01:53:58+01:00 Download 8a446d5
Download de80e13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T17:43:47+01:00 Download 09fe8dd
Download 43b024c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T16:38:34+01:00 Download 5ebe149
Download 3fef9b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:28:30+01:00 Download b210a94
Download 8b3827f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:06:18+01:00 Download 6a89236
Download 788d3df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:27:41+01:00 Download db74254
Download 3e71ca0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:06:03+01:00 Download 785ec61
Download 6a89236 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-05T21:25:02+01:00

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

Trying to find witnesses for program (bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685, sv-benchmarks/c/float-benchs/float_double_true-unreach-call_true-termination.c).

Found 29 witnesses for program sv-benchmarks/c/float-benchs/float_double_true-unreach-call_true-termination.c, bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c6b1ba3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 5 2017-12-01T23:39:10+01:00
Download 09fe8dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:26 CET (sv-comp)
Download bd78c2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 4 2017-12-03T01:00Z
Download c1caeaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-01T23:20 CET (sv-comp)
Download 213b560 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 4 2017-12-02T08:03Z
Download 1370116 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T15:38:16.085560
Download ce4acd0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T20:52:22.007460
Download d2c2207 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-02T21:31:45+01:00
Download 81b9d40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-11-30T22:47:04+01:00
Download 459b821 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T06:59:56+01:00 aa82436
Download a1a8456 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T04:08:40+01:00 41eef6e
Download c20fea3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T02:45:17+01:00 e94414d
Download 2bdcb53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T02:19:35+01:00 f7a2f69
Download 93d9272 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T20:12:17+01:00 117f760
Download 744cc49 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T09:03:41+01:00 06ef246
Download 46e44a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T00:04:33+01:00 c77f316
Download e550c5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T22:24:11+01:00 a354cb6
Download dafc043 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T08:14:07+01:00 9dc0205
Download 68e12ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T06:36:29+01:00 984478e
Download 3869ff2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T06:26:34+01:00 1074aa8
Download 5e04dbb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T04:52:08+01:00 f8dd343
Download e328d36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T04:35:12+01:00 c2a61f3
Download 07baf20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T04:27:26+01:00 97ca8b9
Download 76aeb98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-11-30T16:59:25+01:00
Download 918ce8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 7 2017-11-30T20:21:35+01:00
Download fb89291 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 4 2017-12-01T02:14:26+01:00
Download 7963786 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 4 2017-11-30T22:50 CET (sv-comp)
Download 52b812d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 4 2017-12-02T00:39Z
Download e7f7833 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 7 2017-11-30T14:47 CET (sv-comp)

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

Trying to find witnesses for program (bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685, sv-benchmarks/c/float-benchs/float_double_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/float_double_true-unreach-call_true-termination.c, bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/bcf407e34f9e43ee2491e1c0efb6e4b8701e274658fc0e882a84d4913c3ae685.json

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