English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Deductive verification has been successful in verifying interestingproperties of real-world programs. One notable gap is the limited support forfloating-point reasoning. This is unfortunate, as floating-point arithmetic isparticularly unintuitive to reason about due to rounding as well as thepresence of the special values infinity and `Not a Number' (NaN). In thispaper, we present the first floating-point support in a deductive verificationtool for the Java programming language. Our support in the KeY verifier handlesarithmetic via floating-point decision procedures inside SMT solvers andtranscendental functions via axiomatization. We evaluate this integration onnew benchmarks, and show that this approach is powerful enough to prove theabsence of floating-point special values -- often a prerequisite for furtherreasoning about numerical computations -- as well as certain functionalproperties for realistic benchmarks.

Deductive Verification of Floating-Point Java Programs in KeY