Computer-assisted verification of four interval arithmetic operators

DOI10.1016/j.cam.2020.112893zbMath1434.65063arXiv2003.10623OpenAlexW3014300714MaRDI QIDQ2175842

Tomohito Yabu, Daisuke Ishii

Publication date: 30 April 2020

Published in: Journal of Computational and Applied Mathematics (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2003.10623

zbMATH Keywords

interval arithmeticprogram verificationSMT solversproof assistantsfloating-point numbers

Mathematics Subject Classification ID

Interval and finite arithmetic (65G30) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Coq
• Why3
• Alt-Ergo
• Flocq
• CRlibm
• kv

Cites Work

• Unnamed Item
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• Interval arithmetic with containment sets
• Derived eigenvalues of symmetric matrices, with applications to distance geometry
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
• A three-tier strategy for reasoning about floating-point numbers in SMT
• Certification of bounds on expressions involving rounded operators
• Multi-Prover Verification of Floating-Point Programs

This page was built for publication: Computer-assisted verification of four interval arithmetic operators