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/float21_true-unreach-call.i
programSHA d284f164d079b56cea9b98b5bf7ddc77416d95b591aac43b8055d4d9e2e7d5d0
witnessName results-validated/cpa-seq-validate-correctness-witnesses-2ls.2018-12-06_0659.logfiles/sv-comp19_prop-reachsafety.float21_true-unreach-call.i.files/witness.graphml
witnessSHA 1adbece97261a6aeefff0dcc952d89b0c7d8295408dbed781c6971519fa3c51f

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T07:48:54+01:00
inputwitnesshash 287879abcb28d63c88e443cf5813faccca4c42f98fe6b62ad41ff817728b9ea4
producer CPAchecker 1.7-svn 29852
program-sha256 d284f164d079b56cea9b98b5bf7ddc77416d95b591aac43b8055d4d9e2e7d5d0
programfile ../../sv-benchmarks/c/floats-cbmc-regression/float21_true-unreach-call.i
programhash d284f164d079b56cea9b98b5bf7ddc77416d95b591aac43b8055d4d9e2e7d5d0
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/1adbece97261a6aeefff0dcc952d89b0c7d8295408dbed781c6971519fa3c51f.graphml
witness-sha256 1adbece97261a6aeefff0dcc952d89b0c7d8295408dbed781c6971519fa3c51f
witness-size 9424
witness-type correctness_witness

This witness was created for this program (cf. table above, d284f164d079b56cea9b98b5bf7ddc77416d95b591aac43b8055d4d9e2e7d5d0).

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 64cd513 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T00:18 CET (comp)
Download 34727a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T20:17:52+01:00 Download ddc4e75
Download fe1a0fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T20:17:22+01:00 Download 17263d9
Download 6bae81c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T20:02:18+01:00 Download b8b62cb
Download e848154 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-08T00:37:43+01:00 Download 41e148d
Download a343a2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-07T23:46:59+01:00 Download 1f25bc5
Download 0f5163e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-07T23:31:02+01:00 Download e534a79
Download f8ad611 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-07T19:39:35+01:00 Download efeb05d
Download 3eb8748 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-05T19:13:06+01:00 Download 1581082
Download e7ee228 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-05T19:03:02+01:00 Download 4302555
Download 1035306 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-04T02:07:59+01:00 Download 64cd513
Download 65942d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-11-30T16:20:05+01:00 Download 1f43a9f
Download 1f43a9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 9 2019-11-30T02:47:44+01:00
Download 41e148d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 9 2019-12-07T13:34:47+01:00
Download ddc4e75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 9 2019-11-30T22:54:12+01:00
Download 1f25bc5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness BRICK 3 2019-12-07T21:39:06Z

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ad407c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T02:49:33
Download d0db125 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T09:34 CET (sv-comp)
Download a1f1d92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 9 2018-12-10T18:41:10+01:00
Download aa62a6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 9 2018-12-07T01:00:55+01:00
Download baeb602 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-10T19:48:44+01:00 Download a1f1d92
Download a1810a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-09T20:21:35+01:00 Download 05a1ba5
Download 7de5e59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-09T17:23:43+01:00 Download cbc576b
Download f772462 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T21:38:43+01:00 Download ad407c4
Download 885f1d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T07:09:34+01:00 Download aa62a6a
Download fc4a6e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T03:31:22+01:00 Download 8621015
Download 5200e2e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-07T17:44:52+01:00 Download c2f4c63
Download 3d6c1f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-07T16:38:29+01:00 Download d0db125
Download e359c34 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:28:58+01:00 Download 91f26e5
Download a07af3d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:15:11+01:00 Download a3357d9
Download 3e8317e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T08:22:03+01:00 Download f9e9624
Download 3b0d438 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T07:50:12+01:00 Download 53ba707
Download 1adbece Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T07:48:54+01:00 Download 287879a
Download a3357d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-05T16:40:01+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a991c31 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T18:56:24+01:00
Download e54cdf4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 5 2017-12-02T11:51:28+01:00
Download 5b4b1be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 29 2017-12-03T04:48Z
Download 18504c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 30 2017-12-02T16:33Z
Download bcd179a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T14:19:04.221984
Download 5110dd4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T09:08:18.951406
Download 3f353ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 11 2017-12-03T00:56:39+01:00
Download 8d7ab0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T07:26:45+01:00
Download c707698 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 11 2017-12-03T06:58:01+01:00 00a8851
Download 1ce25cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 11 2017-12-03T04:26:32+01:00 20d27c0
Download 2543aa9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 11 2017-12-03T02:23:21+01:00 6e5d8d5
Download 0610d11 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 11 2017-12-03T00:52:02+01:00 c02a0e6
Download ed23e64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 11 2017-12-02T08:50:04+01:00 8edb75d
Download 809c4c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 11 2017-12-01T22:21:52+01:00 d3817ca
Download 96bdd20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 11 2017-12-01T08:13:32+01:00 2f6e2a5
Download aeb733e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 11 2017-12-01T06:41:59+01:00 8d9c57f
Download 04a21f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 11 2017-12-01T05:28:52+01:00 3b683ab
Download c5fbe74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 11 2017-12-01T05:10:16+01:00 7e03ecf
Download 01ff031 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 11 2017-11-30T22:31:12+01:00
Download f6343af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 11 2017-11-30T11:50 CET (sv-comp)
Download 0edfda1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 29 2017-12-02T17:28Z
Download 349a099 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 60 2017-11-30T14:35 CET (sv-comp)

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

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

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

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