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 Tools annual

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 Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Test instability in a floating-point program occurs when the control flow ofthe program diverges from its ideal execution assuming real arithmetic. Thisphenomenon is caused by the presence of round-off errors that affect theevaluation of arithmetic expressions occurring in conditional statements.Unstable tests may lead to significant errors in safety-critical applicationsthat depend on numerical computations. Writing programs that take intoconsideration test instability is a difficult task that requires expertise onfinite precision computations and rounding errors. This paper presents atoolchain to automatically generate and verify a provably correct test-stablefloating-point program from a functional specification in real arithmetic. Theinput is a real-valued program written in the Prototype Verification System(PVS) specification language and the output is a transformed floating-point Cprogram annotated with ANSI/ISO C Specification Language (ACSL) contracts.These contracts relate the floating-point program to its functionalspecification in real arithmetic. The transformed program detects if unstabletests may occur and, in these cases, issues a warning and terminate. Anapproach that combines the Frama-C analyzer, the PRECiSA round-off errorestimator, and PVS is proposed to automatically verify that the generatedprogram code is correct in the sense that, if the program terminates without awarning, it follows the same computational path as its real-valued functionalspecification.

Automatic generation and verification of test-stable floating-point code