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/float14_true-unreach-call.i
programSHA 00a65caf163cee72b7f58c01c623bfd367123a6ea6484cfbd8fbb0296bda136f
witnessName results-verified/esbmc-kind.2018-12-06_1103.logfiles/sv-comp19_prop-reachsafety.float14_true-unreach-call.i.files/witness.graphml
witnessSHA 96cca20cb688d1827826d357ff7abff8cc1c652ae43bd93e01d44cde639578ab

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-07T19:23:14.671071
producer ESBMC 6.0.0 kind
programfile ../../sv-benchmarks/c/floats-cbmc-regression/float14_true-unreach-call.i
programhash fc29bd9cd4b6bebb444bcb0c8a01e26fdfb66041
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/96cca20cb688d1827826d357ff7abff8cc1c652ae43bd93e01d44cde639578ab.graphml
witness-sha256 96cca20cb688d1827826d357ff7abff8cc1c652ae43bd93e01d44cde639578ab
witness-size 3404
witness-type correctness_witness

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

Trying to find witnesses for program (00a65caf163cee72b7f58c01c623bfd367123a6ea6484cfbd8fbb0296bda136f, sv-benchmarks/c/floats-cbmc-regression/float14_true-unreach-call.i).

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

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

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

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

Found 16 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float14_true-unreach-call.i, 00a65caf163cee72b7f58c01c623bfd367123a6ea6484cfbd8fbb0296bda136f
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/00a65caf163cee72b7f58c01c623bfd367123a6ea6484cfbd8fbb0296bda136f.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5e02cc0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T00:57 CET (comp)
Download 5110f38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:17:58+01:00 Download 73be589
Download 8170c42 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:15:13+01:00 Download 60624d2
Download b6734bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:02:49+01:00 Download 6877f85
Download 0393248 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-08T00:41:42+01:00 Download 14645ce
Download 15a5baf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:46:35+01:00 Download 2c58eaa
Download 972ae7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:33:36+01:00 Download 6bfdc13
Download 65fc79a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T19:42:23+01:00 Download 7888773
Download 14550bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:13:14+01:00 Download 763587a
Download a112593 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:02:56+01:00 Download a6c71e7
Download 9a6f7d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-04T02:07:31+01:00 Download 5e02cc0
Download 870b634 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-11-30T16:11:32+01:00 Download 649a0ed
Download 649a0ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 3 2019-11-30T01:37:06+01:00
Download 14645ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 3 2019-12-07T19:57:10+01:00
Download 73be589 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 4 2019-12-01T14:56:00+01:00
Download 2c58eaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness BRICK 3 2019-12-07T21:40:28Z

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

Trying to find witnesses for program (00a65caf163cee72b7f58c01c623bfd367123a6ea6484cfbd8fbb0296bda136f, sv-benchmarks/c/floats-cbmc-regression/float14_true-unreach-call.i).

Found 16 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float14_true-unreach-call.i, 00a65caf163cee72b7f58c01c623bfd367123a6ea6484cfbd8fbb0296bda136f
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/00a65caf163cee72b7f58c01c623bfd367123a6ea6484cfbd8fbb0296bda136f.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a9120eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T06:29:12
Download b079bf8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T06:31 CET (sv-comp)
Download 3b2cc58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-07T07:44:25+01:00
Download 9c99c72 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-10T20:05:34+01:00 Download ec334f3
Download 46b9906 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:23:32+01:00 Download 352b228
Download 9b3e6f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:11:02+01:00 Download d69c87a
Download 4ec2ea7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T21:30:52+01:00 Download a9120eb
Download 90cb7e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T05:20:22+01:00 Download 3b2cc58
Download 4b574ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T02:40:20+01:00 Download 96cca20
Download fbe2a2e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T17:46:01+01:00 Download 2154d54
Download ff3ef63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T16:39:22+01:00 Download b079bf8
Download 15ac7db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:29:03+01:00 Download afa200b
Download 92a49c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:45:28+01:00 Download 4acc5b4
Download 48b77d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:24:39+01:00 Download 3f17882
Download 4b702ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T07:11:45+01:00 Download b1315a0
Download 4acc5b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T06:06:25+01:00

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

Trying to find witnesses for program (00a65caf163cee72b7f58c01c623bfd367123a6ea6484cfbd8fbb0296bda136f, sv-benchmarks/c/floats-cbmc-regression/float14_true-unreach-call.i).

Found 25 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float14_true-unreach-call.i, 00a65caf163cee72b7f58c01c623bfd367123a6ea6484cfbd8fbb0296bda136f
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/00a65caf163cee72b7f58c01c623bfd367123a6ea6484cfbd8fbb0296bda136f.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6b2fc7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 5 2017-12-02T10:12:19+01:00
Download a9dd6d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 10 2017-12-03T03:18Z
Download 4d66589 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 10 2017-12-02T18:49Z
Download 2493dad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T03:18:23.336520
Download 24d3e4c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T10:42:53.561498
Download ca54bc4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 3 2017-12-02T19:06:02+01:00
Download 7df812e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T07:20:24+01:00
Download f02ac56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T06:51:38+01:00 65ad2cf
Download 1358688 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T04:00:28+01:00 fc9a48b
Download c3da34f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T02:59:09+01:00 522955c
Download 87c88b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T02:01:29+01:00 ca5422f
Download 71faf9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T08:18:04+01:00 fe623da
Download 3bafe04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T22:27:47+01:00 9626e1b
Download 5409e04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T08:13:21+01:00 9bdee6e
Download ada15b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T07:15:52+01:00 f6375ee
Download 16b9ec5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T06:21:28+01:00 1b5a356
Download 76eecfa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T06:10:25+01:00 db0c92b
Download a2bafc5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T04:46:12+01:00 ad9978d
Download cd1fc66 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T04:42:24+01:00 1fe7c82
Download ba3ce32 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-11-30T18:08:23+01:00
Download e4d42ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 10 2017-11-30T12:35:50+01:00
Download 5b9c084 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 4 2017-11-30T13:17:58+01:00
Download 055f3e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 5 2017-11-30T13:33 CET (sv-comp)
Download d8b3bf2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 10 2017-12-02T07:47Z
Download b61dba6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 24 2017-11-30T22:06 CET (sv-comp)

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

Trying to find witnesses for program (00a65caf163cee72b7f58c01c623bfd367123a6ea6484cfbd8fbb0296bda136f, sv-benchmarks/c/floats-cbmc-regression/float14_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float14_true-unreach-call.i, 00a65caf163cee72b7f58c01c623bfd367123a6ea6484cfbd8fbb0296bda136f
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/00a65caf163cee72b7f58c01c623bfd367123a6ea6484cfbd8fbb0296bda136f.json

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