Affine Arithmetic and Applications to Real-Number Proving

DOI10.1007/978-3-319-22102-1_20zbMath1465.65042OpenAlexW2143848809MaRDI QIDQ2945641

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

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

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

Related Items

Refinement to certify abstract interpretations: illustrated on linearization for polyhedra

Uses Software

• PVS

Cites Work

• Unnamed Item
• Unnamed Item
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• Provably correct conflict prevention bands algorithms
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• Formalization of Bernstein polynomials and applications to global optimization
• Affine arithmetic: concepts and applications
• Trusting computations: a mechanized proof from partial differential equations to actual program
• Proving Bounds on Real-Valued Functions with Computations
• Introduction to Interval Analysis
• Formal Verification of an Optimal Air Traffic Conflict Resolution and Recovery Algorithm
• Algorithm 795
• Verified Real Number Calculations: A Library for Interval Arithmetic
• Efficient Formal Verification of Bounds of Linear Programs