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/Rump_float_true-unreach-call_true-termination.c
programSHA 8433392c57485f063fee67bd43badd5a13b3bcff2d37085ab197042642c9f3e1
witnessName results-verified/cbmc-path.2018-12-04_2245.logfiles/sv-comp19_prop-reachsafety.Rump_float_true-unreach-call_true-termination.c.files/witness.graphml
witnessSHA e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855

Information about the Witness from Competition Database

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

Key Value
creationtime 2018-12-05T13:03 CET (sv-comp)
error-programhash Key 'programhash' not present.
error-specification-exists Key 'specification' not present.
error-xmlparsing File produces XML parsing error.
witness-file witnessFileByHash/e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855.graphml
witness-sha256 e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855
witness-size 0

The following keys are missing in the witness XML file: witness-type, sourcecodelang, producer, specification, programfile, programhash, architecture.

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 77cd19e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T00:04 CET (comp)
Download 9059fa2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:24:33+01:00 Download 50a8fda
Download 8af9250 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:15:09+01:00 Download ec35782
Download 4d4b0f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:02:27+01:00 Download 123df7a
Download 777e87a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-08T00:36:25+01:00 Download 1e8fb44
Download c5fe5d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:47:35+01:00 Download ffbb1da
Download 70028ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:42:50+01:00 Download 3c3b22b
Download 019a69b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T19:39:41+01:00 Download 2fe06dc
Download 361c040 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:13:11+01:00 Download 5fc87fb
Download 2fd1339 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:03:11+01:00 Download f893eaa
Download 0af68c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-04T02:07:49+01:00 Download 77cd19e
Download ea0332e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-11-30T19:56:48+01:00 Download 54d1bef
Download 20f0a7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-11-30T17:14:35+01:00 Download f7ec163
Download f7ec163 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 4 2019-11-30T14:52:36+01:00
Download 1e8fb44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 4 2019-12-07T19:59:35+01:00
Download ec35782 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 4 2019-12-01T09:22:31+01:00
Download ffbb1da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness BRICK 3 2019-12-07T21:36:38Z

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

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

Found 20 witnesses for program sv-benchmarks/c/float-benchs/Rump_float_true-unreach-call_true-termination.c, 8433392c57485f063fee67bd43badd5a13b3bcff2d37085ab197042642c9f3e1
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/8433392c57485f063fee67bd43badd5a13b3bcff2d37085ab197042642c9f3e1.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2000e36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T03:28 CET (sv-comp)
Download bbd28a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T09:42:18
Download e93a278 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T01:27 CET (sv-comp)
Download edb87a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-08T04:25:22+01:00
Download 8774301 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-10T20:00:50+01:00 Download c26095c
Download 50998b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-10T10:31:13+01:00 Download e4e6fc9
Download 189e8e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:22:12+01:00 Download 6e219f8
Download f10f6c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:03:32+01:00 Download ca46571
Download cce3eea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T23:10:44+01:00 Download 2000e36
Download b57de78 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T21:28:17+01:00 Download bbd28a7
Download 6d73ad2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T05:33:41+01:00 Download edb87a0
Download 4b4a4df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T03:02:53+01:00 Download c3f2daa
Download 4fab90b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T01:52:32+01:00 Download e4e6fc9
Download d717aec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T17:44:46+01:00 Download 22c932b
Download 38cef95 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T16:38:18+01:00 Download e93a278
Download 69106e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:28:16+01:00 Download fd98d6f
Download 6d94f62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:45:59+01:00 Download 33bd704
Download 8636914 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:23:37+01:00 Download 6036650
Download f02ed41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:11:13+01:00 Download d78d560
Download 33bd704 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-05T22:53:31+01:00

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

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

Found 27 witnesses for program sv-benchmarks/c/float-benchs/Rump_float_true-unreach-call_true-termination.c, 8433392c57485f063fee67bd43badd5a13b3bcff2d37085ab197042642c9f3e1
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/8433392c57485f063fee67bd43badd5a13b3bcff2d37085ab197042642c9f3e1.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f3f84d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 5 2017-12-02T11:17:25+01:00
Download 22c932b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T23:52 CET (sv-comp)
Download 46a1b6d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 5 2017-12-03T05:23Z
Download 93bc37d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T13:22 CET (sv-comp)
Download 04f4b78 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T12:41:53.469914
Download 1d15aeb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T08:34:42.957676
Download 428a338 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-02T18:32:09+01:00
Download 303ea53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T07:28:24+01:00
Download 22c62b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T06:51:25+01:00 a2a9311
Download a0ada0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T04:30:20+01:00 0621a8b
Download 7352f14 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T02:23:33+01:00 2553309
Download c402fa8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T20:05:42+01:00 0953c42
Download 1ac3960 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T08:31:41+01:00 25c9e4b
Download ba2d459 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T00:04:28+01:00 feea157
Download 5e6632c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T22:23:28+01:00 834011b
Download c252a04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T08:13:28+01:00 c29d91f
Download 94f8a29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T07:14:28+01:00 7c66115
Download 6add536 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T06:22:50+01:00 a56e90a
Download 8738315 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T05:29:46+01:00 713109a
Download b98e7b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T05:20:34+01:00 dfe6255
Download edd9445 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T05:14:02+01:00 8ca90d9
Download bbda355 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-11-30T21:10:06+01:00
Download 8331e36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 9 2017-11-30T13:49:54+01:00
Download 6eeb2ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 4 2017-11-30T17:04:51+01:00
Download 5e73fdd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 5 2017-11-30T13:28 CET (sv-comp)
Download cc4e2d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 5 2017-12-02T19:11Z
Download 080b161 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 8 2017-11-30T14:18 CET (sv-comp)

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

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

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

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