Computer-assisted verification of four interval arithmetic operators

JOURNAL OF COMPUTATIONAL AND APPLIED MATHEMATICS

卷:377

Article

Ishii, Daisuke^1,2  Yabu, Tomohito¹ 

[1] Univ Fukui, Dept Informat Sci, 3-9-1 Bunkyo, Fukui, Fukui 9108507, Japan

[2] Japan Adv Inst Sci & Technol, 1-1 Asahidai, Nomi, Ishikawa 9231292, Japan

关键词: Interval arithmetic;    Floating-point numbers;    Program verification;    SMT solvers;    Proof assistants;   

DOI  :  10.1016/j.cam.2020.112893

来源: Elsevier

【 摘 要 】

Interval arithmetic libraries provide the four elementary arithmetic operators for operand intervals bounded by floating-point numbers. Actual implementations need to make a large case analysis that considers, e.g., magnitude relations between all pairs of argument bounds, positional relations between the arguments and zero, and handling of the special values, +/-infinity and NaN. Their correctness is not obvious as they are implemented by human hands, which comes to be critical for the reliability. This work provides a mechanically-verified interval arithmetic library. For this purpose, we utilize the Why3 platform equipped with a specification language for annotated programs and back-end theorem provers. We conduct several proof tasks for each of three properties of the target code: validity, soundness, and tightness; zero division exception handling is also verified for the division code. To accomplish the proof, we propose several techniques for specification/verification. First, we specify additional lemmas that support deductions made by back-end SMT solvers, which enable to discharge proof obligations in floating-point arithmetic containing nonlinear terms. Second, we examine the annotation of tightness, which requires to assume that a computation may result in NaN; we propose specific extremum operators for this purpose. In the experiments, applying the techniques in conjunction with the Alt-Ergo SMT solver and the Coq proof assistant proved the entire code. (C) 2020 Elsevier B.V. All rights reserved.

【 授权许可】

Free