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/

Zendy Plus

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

Zendy Tools

Zendy Open

We give a process for verifying numerical programs against their functionalspecifications. Our implementation is capable of automatically verifyingprograms against tight error bounds featuring common elementary functions. Wedemonstrate and evaluate our implementation on several examples, yielding thefirst fully verified SPARK implementations of the sine and square rootfunctions. The process integrates existing tools using a series oftransformations and derivations, building on the proving process in SPARK whereWhy3 produces Verification Conditions (VCs) and tools such as SMT solversattempt to verify them. We add steps aimed specifically at VCs that containinequalities with both floating-point operations and exact real functions.PropaFP is our open-source implementation of these steps. The steps includesymbolic simplifications, deriving bounds via interval arithmetic, and safelyreplacing floating-point operations with exact operations, utilizing tools suchas FPTaylor or Gappa to bound the compound rounding errors of expressions.Finally, the VCs are passed to provers such as dReal, MetiTarski or LPPaverwhich attempt to complete the proof or suggest possible counter-examples.

Auto-active Verification of Floating-point Programs via Nonlinear Real Provers