Affine arithmetic and applications to real-number proving

DOI10.1007/978-3-319-22102-1_20MaRDI QIDQ2945641zbMATH OpenOpenAlexFDO

Authors Andrew Paul Smith, Mariano M. Moscato, César Muñoz

Publication date 14 September 2015

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-22102-1_20

Mathematics Subject Classification ID

Algorithms with automatic result verification (65G20) Interval and finite arithmetic (65G30) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• An Introduction to Affine Arithmetic
• scientific article; zbMATH DE number 1408651
• Theorem Proving in Higher Order Logics
• Affine arithmetic: concepts and applications
• Using PVS to validate the algorithms of an exact arithmetic.

Cites work

• Affine arithmetic: concepts and applications
• Algorithm 795
• Efficient formal verification of bounds of linear programs
• Formal Verification of an Optimal Air Traffic Conflict Resolution and Recovery Algorithm
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• Formalization of Bernstein polynomials and applications to global optimization
• scientific article; zbMATH DE number 1190534 (Why is no real title available?)
• scientific article; zbMATH DE number 1408651 (Why is no real title available?)
• Introduction to Interval Analysis
• Provably correct conflict prevention bands algorithms
• Proving Bounds on Real-Valued Functions with Computations
• Trusting computations: a mechanized proof from partial differential equations to actual program
• Verified Real Number Calculations: A Library for Interval Arithmetic
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program

Cited in

(15)

• A new algorithm for Chebyshev minimum-error multiplication of reduced affine forms
• Refinement to certify abstract interpretations: illustrated on linearization for polyhedra
• Using PVS to validate the algorithms of an exact arithmetic.
• A validated real function calculus
• Computer-assisted verification of four interval arithmetic operators
• Affine arithmetic: concepts and applications
• Real Algebraic Strategies for MetiTarski Proofs
• scientific article; zbMATH DE number 5693751 (Why is no real title available?)
• Under-Approximations of Computations in Real Numbers Based on Generalized Affine Arithmetic
• Self-verified extension of affine arithmetic to arbitrary order
• A generalization of \(p\)-boxes to affine arithmetic
• scientific article; zbMATH DE number 1408651 (Why is no real title available?)
• An Introduction to Affine Arithmetic
• Embedding differential dynamic logic in PVS
• A revised monotonicity-based method for computing tight image enclosures of functions

Describes a project that uses

Uses Software

• PVS

This page was built for publication: Affine arithmetic and applications to real-number proving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2945641)