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/float6_true-unreach-call_true-termination.i
programSHA 8f9d534a62e398d4eff466ed1117fbed7b4bb8f0e33a72038ddfd71f849ac51c
witnessName results-validated/cpa-seq-validate-correctness-witnesses-veriabs.2018-12-10_1933.logfiles/sv-comp19_prop-reachsafety.float6_true-unreach-call_true-termination.i.files/witness.graphml
witnessSHA e323304ae75762992112f89341594456b5db4ab466a2870ba841791b3f70bae3

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-10T20:10:02+01:00
inputwitnesshash f809c49a1d56b896ccd40b8085a09d8edec0a2330e5fcc0e205dd26423e8b0db
producer CPAchecker 1.7-svn 29852
program-sha256 8f9d534a62e398d4eff466ed1117fbed7b4bb8f0e33a72038ddfd71f849ac51c
programfile ../../sv-benchmarks/c/floats-cbmc-regression/float6_true-unreach-call_true-termination.i
programhash 8f9d534a62e398d4eff466ed1117fbed7b4bb8f0e33a72038ddfd71f849ac51c
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/e323304ae75762992112f89341594456b5db4ab466a2870ba841791b3f70bae3.graphml
witness-sha256 e323304ae75762992112f89341594456b5db4ab466a2870ba841791b3f70bae3
witness-size 11666
witness-type correctness_witness

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

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

Trying to find witnesses for program (8f9d534a62e398d4eff466ed1117fbed7b4bb8f0e33a72038ddfd71f849ac51c, sv-benchmarks/c/floats-cbmc-regression/float6_true-unreach-call_true-termination.i).

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

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

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

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

Found 0 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float6_true-unreach-call_true-termination.i, 8f9d534a62e398d4eff466ed1117fbed7b4bb8f0e33a72038ddfd71f849ac51c
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/8f9d534a62e398d4eff466ed1117fbed7b4bb8f0e33a72038ddfd71f849ac51c.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 '19

Trying to find witnesses for program (8f9d534a62e398d4eff466ed1117fbed7b4bb8f0e33a72038ddfd71f849ac51c, sv-benchmarks/c/floats-cbmc-regression/float6_true-unreach-call_true-termination.i).

Found 19 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float6_true-unreach-call_true-termination.i, 8f9d534a62e398d4eff466ed1117fbed7b4bb8f0e33a72038ddfd71f849ac51c
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/8f9d534a62e398d4eff466ed1117fbed7b4bb8f0e33a72038ddfd71f849ac51c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 058572d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T01:01:50
Download 984a799 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-06T20:47 CET (sv-comp)
Download 97882f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 12 2018-12-07T21:36:23+01:00
Download e323304 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-10T20:10:02+01:00 Download f809c49
Download 6780197 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-09T20:17:09+01:00 Download 6577a0a
Download 60975e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-09T20:08:53+01:00 Download 5c0cc9a
Download 9121988 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-09T19:53:06+01:00 Download 65b998f
Download f3bcae2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-08T21:40:31+01:00 Download 058572d
Download 1e4547b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-08T05:48:18+01:00 Download 97882f3
Download 3082d46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-08T03:08:15+01:00 Download 68fd7de
Download 0a49f6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-07T17:44:09+01:00 Download 7256d29
Download 1c2167b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-07T16:38:58+01:00 Download 984a799
Download 6ccc9a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-06T09:28:43+01:00 Download 6824c27
Download c47477a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-06T09:01:08+01:00 Download e8d1d98
Download 54ff1ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-06T08:25:17+01:00 Download 85baa96
Download 406ea80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-06T08:02:09+01:00 Download 09bdf7a
Download c2e22b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-06T07:49:16+01:00 Download 4fc52b4
Download e8d1d98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 12 2018-12-05T14:57:28+01:00
Download 37bd2a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-06T20:49 CET (sv-comp)

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

Trying to find witnesses for program (8f9d534a62e398d4eff466ed1117fbed7b4bb8f0e33a72038ddfd71f849ac51c, sv-benchmarks/c/floats-cbmc-regression/float6_true-unreach-call_true-termination.i).

Found 31 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float6_true-unreach-call_true-termination.i, 8f9d534a62e398d4eff466ed1117fbed7b4bb8f0e33a72038ddfd71f849ac51c
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/8f9d534a62e398d4eff466ed1117fbed7b4bb8f0e33a72038ddfd71f849ac51c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download be6fa63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 32 2017-12-03T02:26Z
Download d91e478 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 32 2017-12-02T10:21Z
Download 64ed2cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T21:36:11.533457
Download c81173c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T12:51:08.960328
Download 74acf46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T01:35:57.447234
Download e3a107e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T16:42:00.384428
Download cb825b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 6 2017-12-01T19:31 CET (sv-comp)
Download fa6c8a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 13 2017-12-03T02:18:29+01:00
Download 77b25f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T03:43:30+01:00
Download 5585e39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-03T06:50:40+01:00 5db4681
Download 054ca47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-03T04:21:40+01:00 0d7e53e
Download 7068d2a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-03T02:09:59+01:00 5756bb2
Download 7071c2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-03T00:39:35+01:00 8690e74
Download dcc1642 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-02T15:27:24+01:00 5c23cf0
Download 8fbfb02 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-02T08:10:21+01:00 82946df
Download 0b12951 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-01T22:30:27+01:00 75e9063
Download 514bd13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-01T08:14:02+01:00 1d2393c
Download bef8138 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-01T05:55:48+01:00 86682cc
Download cb1355f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-01T05:23:26+01:00 87f6819
Download 6056b15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-01T05:21:50+01:00 04df378
Download c0b8d06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-01T05:10:25+01:00 17432b3
Download 29542a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-12-01T04:34:57+01:00 ddc0101
Download 0aceb3b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 13 2017-11-30T15:57:20+01:00
Download 0eb78e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 24 2017-11-30T11:45:52+01:00
Download e452335 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 13 2017-12-01T02:18:30+01:00
Download 6c3791d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 13 2017-12-01T20:52:11+01:00
Download d7a230e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 17 2017-11-30T15:10 CET (sv-comp)
Download 150a993 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 32 2017-12-02T21:23Z
Download c969fb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 15 2017-11-30T23:45 CET (sv-comp)
Download 690eeda Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 12 2017-12-01T17:10 CET (sv-comp)
Download 7f0717f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 15 2017-12-01T15:53 CET (sv-comp)

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

Trying to find witnesses for program (8f9d534a62e398d4eff466ed1117fbed7b4bb8f0e33a72038ddfd71f849ac51c, sv-benchmarks/c/floats-cbmc-regression/float6_true-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cbmc-regression/float6_true-unreach-call_true-termination.i, 8f9d534a62e398d4eff466ed1117fbed7b4bb8f0e33a72038ddfd71f849ac51c
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/8f9d534a62e398d4eff466ed1117fbed7b4bb8f0e33a72038ddfd71f849ac51c.json

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