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/inv_sqrt_Quake_true-unreach-call_true-termination.c
programSHA 08a67ae40fc31d82508b839f685d427523122e3599ca3b569edde085f9e22b6a
witnessName results-verified/cbmc-path.2018-12-04_2245.logfiles/sv-comp19_prop-reachsafety.inv_sqrt_Quake_true-unreach-call_true-termination.c.files/witness.graphml
witnessSHA 6c5f748ae3c174e656f0775fb79ff163c898210eacc39d4c471ff7dc11d1cb73

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-05T00:45 CET (sv-comp)
producer CBMC
programfile ../../sv-benchmarks/c/float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c
programhash e0f1bd2a42710b6c2eba96cb622bd79ffd05436a
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/6c5f748ae3c174e656f0775fb79ff163c898210eacc39d4c471ff7dc11d1cb73.graphml
witness-sha256 6c5f748ae3c174e656f0775fb79ff163c898210eacc39d4c471ff7dc11d1cb73
witness-size 7133
witness-type correctness_witness

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

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

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

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

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

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

Found 15 witnesses for program sv-benchmarks/c/float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c, 08a67ae40fc31d82508b839f685d427523122e3599ca3b569edde085f9e22b6a
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/08a67ae40fc31d82508b839f685d427523122e3599ca3b569edde085f9e22b6a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0b1a32e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T22:22 CET (comp)
Download 288683e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:17:53+01:00 Download e1239b6
Download 8475531 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:07:14+01:00 Download 402e60e
Download dbb0c14 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:02:16+01:00 Download 6754377
Download 5e4a65a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T00:37:31+01:00 Download eb58b0f
Download 59cd68f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T23:45:41+01:00 Download 967d28c
Download 9e7525f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T19:13:24+01:00 Download 529caa1
Download a985ea7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T19:02:54+01:00 Download 1a388f9
Download ce09190 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-04T02:07:59+01:00 Download 0b1a32e
Download 433c350 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-11-30T19:25:36+01:00 Download 7d87786
Download e3e9d9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-11-30T16:33:11+01:00 Download e344948
Download e344948 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 6 2019-11-30T01:58:55+01:00
Download eb58b0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 6 2019-12-07T14:57:23+01:00
Download 402e60e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 6 2019-12-01T06:40:40+01:00
Download 967d28c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness BRICK 3 2019-12-07T21:35:28Z

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

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

Found 18 witnesses for program sv-benchmarks/c/float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c, 08a67ae40fc31d82508b839f685d427523122e3599ca3b569edde085f9e22b6a
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/08a67ae40fc31d82508b839f685d427523122e3599ca3b569edde085f9e22b6a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 735f9a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T00:13:10
Download 18cd43e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T05:41 CET (sv-comp)
Download db150fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 6 2018-12-10T17:38:15+01:00
Download 5b02825 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-07T10:48:43+01:00
Download 9fbdd72 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-10T19:49:46+01:00 Download db150fe
Download 4dc123a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:14:35+01:00 Download eefe4ae
Download b1806a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T17:14:40+01:00 Download 40099f5
Download c3a15a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T21:40:59+01:00 Download 735f9a4
Download b9c7532 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T05:10:52+01:00 Download 5b02825
Download 9db0a83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T03:44:34+01:00 Download ee62a79
Download 8824fef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T17:46:01+01:00 Download 5aad9f5
Download ecfcf41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T16:38:28+01:00 Download 18cd43e
Download 37c6a86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:28:16+01:00 Download 6717252
Download 627e0fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:55:55+01:00 Download 39a8c04
Download cd5b878 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:26:16+01:00 Download 6c5f748
Download b30a643 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T07:53:27+01:00 Download 0652651
Download 3d091fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T07:06:25+01:00 Download 34fcb1a
Download 39a8c04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-05T15:20:18+01:00

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

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

Found 16 witnesses for program sv-benchmarks/c/float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c, 08a67ae40fc31d82508b839f685d427523122e3599ca3b569edde085f9e22b6a
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/08a67ae40fc31d82508b839f685d427523122e3599ca3b569edde085f9e22b6a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8cd6f38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 7 2017-12-01T05:37:45+01:00
Download e381f12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 14 2017-11-30T12:50:09+01:00
Download 89bfa7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 6 2017-11-30T15:00:13+01:00
Download 3c59d5a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 7 2017-12-02T00:40:03+01:00
Download c15be39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T23:00:34.315315
Download c372d37 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T19:49:14.008928
Download 1f11857 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 7 2017-12-02T19:23:28+01:00
Download abdb669 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-03T04:23:57+01:00 89b45ca
Download aa62d27 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-02T07:26:04+01:00 8a68aa8
Download e9bcdf2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T22:29:36+01:00 b53f417
Download 5709a56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T07:12:39+01:00 8460c94
Download ff6c23c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T06:44:42+01:00 2cf0638
Download a98221b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T05:00:56+01:00 fa0a4a0
Download ae8f95e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T02:38:37+01:00
Download 1f7074e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 7 2017-11-30T22:18 CET (sv-comp)
Download edc5c6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 11 2017-11-30T22:54 CET (sv-comp)

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

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

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

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