Improved bound for stochastic formal correctness of numerical algorithms

Marc Daumas, David Lester, Érik Martin-Dorel, Annick Truffert

    Research output: Contribution to journalArticlepeer-review


    We provide bounds on the probability that accumulated errors were never above a given threshold on numerical algorithms. Such algorithms are used, for example, in aircraft and nuclear power plants. This report contains simple formulas based on Lévy's, Markov's and Hoeffding's inequalities and it presents a formal theory of random variables with a special focus on producing concrete results. We select three very common applications that cover the common practices of systems that evolve for a long time. We compute the number of bits that remain continuously significant in the first two applications with a probability of failure around one out of a billion, where worst case analysis considers that no significant bit remains. We are using PVS as such formal tools force explicit statement of all hypotheses and prevent incorrect uses of theorems. © 2010 Springer-Verlag London Limited.
    Original languageEnglish
    Pages (from-to)173-179
    Number of pages6
    JournalInnovations in Systems and Software Engineering
    Issue number3
    Publication statusPublished - 2010


    • Certification
    • Formal methods
    • Hybrid systems
    • Probability
    • Round-off error


    Dive into the research topics of 'Improved bound for stochastic formal correctness of numerical algorithms'. Together they form a unique fingerprint.

    Cite this