Author Description

Floating-point representation is widely used in modern days to emulate arithmetic over reals. Unfortunately, floating-point arithmetic leads to rounding errors that propagate and accumulate during execution. Even though floating-point programs may work properly with rounding errors in most cases, there are situations in which the accumulation of rounding errors may lead to catastrophic failures in the real world. In this dissertation, we consider a program failure that is caused by floating-point arithmetic as a numerical bug. This dissertation aims to understand numerical bugs that appear in real-world applications, and more importantly, improve the reliability and efficiency of floating-point programs via program analysis. This work starts with an empirical study of five widely used real-world numerical software libraries to understand the characteristics of numerical bugs. Numerical bugs are known to be particularly difficult to diagnose and fix. Understanding the characteristics of numerical bugs is the first step to combat them more effectively. In the study, we propose a categorization of numerical bugs, and discuss their frequency, symptoms and fixes. To the best of our knowledge, this is the first comprehensive study of real-world numerical bugs. The second part of this dissertation focuses on generating error-inducing inputs to expose and maximize the numerical error in the program output. Such error-inducing inputs are important in testing and debugging floating-point programs. Specifically, we formulate the problem of generating high error-inducing floating-point inputs as a code coverage maximization problem. The code coverage maximization problem has been widely explored and can be solved using symbolic execution. Our key insight is that by injecting inaccuracy checks after floating-point arithmetic operations, we force the symbolic execution engine to explore the probability of the occurrence of severe rounding errors and numerical cancellations in dif