Computer Arithmetic and Formal Proofs ：Verifying Floating-point Algorithms with the Coq System

Publication subTitle ：Verifying Floating-point Algorithms with the Coq System

Author： Boldo Sylvie;Melquiond Guillaume

Publisher： Elsevier Science‎

Publication year： 2017

E-ISBN: 9780081011706

P-ISBN(Paperback): 9781785481123

Subject： O158 Discrete Mathematics;TP3 Computers

Keyword：离散数学,计算技术、计算机技术

Language： ENG

Access to resources Favorite

Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.

Description

Floating-point arithmetic is ubiquitous in modern computing, as it is the tool of choice to approximate real numbers. Due to its limited range and precision, its use can become quite involved and potentially lead to numerous failures. One way to greatly increase confidence in floating-point software is by computer-assisted verification of its correctness proofs.

This book provides a comprehensive view of how to formally specify and verify tricky floating-point algorithms with the Coq proof assistant. It describes the Flocq formalization of floating-point arithmetic and some methods to automate theorem proofs. It then presents the specification and verification of various algorithms, from error-free transformations to a numerical scheme for a partial differential equation. The examples cover not only mathematical algorithms but also C programs as well as issues related to compilation.

Describes the notions of specification and weakest precondition computation and their practical use
Shows how to tackle algorithms that extend beyond the realm of simple floating-point arithmetic
Includes real analysis and a case study about numerical analysis

Chapter

Front Cover

Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System

1 Floating-Point Arithmetic

1.1. FP numbers as real numbers

1.2. Error analysis

1.3. Exceptional values

1.4. Additional definitions and properties

2 The Coq System

2.1. A brief overview of the system

2.2. Tactics

2.3. Standard library

3 Formalization of Formats and Basic Operators

3.1. FP formats and their properties

3.2. Rounding operators and their properties

3.3. How to perform basic FP operations

3.4. IEEE-754 binary formats and operators

4 Automated Methods

4.1. Algebraic manipulations

4.2. Interval arithmetic

4.3. Bounds on round-off error

5 Error-Free Computations and Applications

5.1. Exact addition and EFT for addition

5.2. EFT for multiplication

5.3. Remainder of the integer division

5.4. Remainders of the FP division and square root

5.5. Taking the square root of the square

5.6. Remainders for the fused-multiply-add (FMA)

6 Example Proofs of Advanced Operators

6.1. Accurate computation of the area of a triangle

6.2. Argument reduction

6.3. Faithful rounding of Horner evaluation

6.4. Integer division computed using FMA

6.5. Average of two FP numbers

6.6. Orientation of three points

6.7. Order-2 discriminant

7 Compilation of FP Programs

7.1. Semantics of languages and FP arithmetic

7.2. Verified compilation

7.3. Conversions between integers and FP numbers

8 Deductive Program Verification

8.1. Introduction

8.2. Our method and tools for program verification

8.3. Examples of annotated programs

8.4. Robustness against compiler optimizations

9 Real and Numerical Analysis

9.1. Running example: three-point scheme for the 1D wave equation

9.2. Advanced formalization of real analysis

9.3. Method error of the 3-point scheme for the 1D wave equation

9.4. Round-off error

9.5. Program verification

Bibliography

Index

Back Cover

The users who browse this book also browse