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, infinities 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.
Towards Efficient Verification of Quantized Neural Networks
Stanford University（斯坦福大学）；Institute of Computing Technology, Chinese Academy of Sciences（中国科学院计算技术研究所）；IT University of Copenhagen（哥本哈根信息技术大学）；National University of Singapore（新加坡国立大学）
Verification of Magnitude and Phase Responses in Fixed-Point Digital Filters
Universidade Federal do Amazonas (UFAM)（亚马孙联邦大学）；Univ. Lille, CNRS, ISEN, Univ. Valenciennes, UMR 8520, IEMN（里尔大学、法国国家科学研究中心、ISEN、瓦朗谢纳大学、IEMN实验室）；Samsung Instituto de P&D da Amazônia (SIDIA)（亚马逊三星研发研究所）
