It is difficult to write a numerical program that does not incur floating-point exceptions in practice. To detect floatingpoint exceptions, most existing methods use static analysis, which may induce false alarms (due to over-approximation), or suffer from scalability issues (since solving floating-point constraints is expensive). Fuzzing is a widely used technique to finding bugs, but existing fuzzing techniques have not yet considered the specific format of floating-point and are lack of guidance for detecting floating-point exceptions. In this paper, we propose a floating-point format aware coverage-based grey-box fuzzing to detect floating-point exceptions for numerical programs. More specifically, we propose a novel mutation strategy for floating-point format aiming at producing valid floating-point test inputs. Moreover, we present a new guidance aiming to search for test inputs that are closer to exposing exceptions. We implement our approach as a tool, named NumFUZZ, based on AFL. We have conducted experiments to evaluate NUMFUZZ on GNU Scientific Library (GSL) and Sun’s C math library respectively. The preliminary experimental results suggest that our approach has promising ability in detecting floating-point exceptions and achieving high floating-point branch coverage in real-world numerical programs.

Analyzing worst-case resource usage of a program is a difficult but important problem. Existing static bound analysis techniques mainly focus on deriving the upper-bound number of visits to a given control location or iterations of a loop. However, there still exist gaps between such bounds and resource usage bounds. In this paper, we present a static analysis approach to derive resource usage bounds for imperative programs. We leverage techniques of program transformation, numerical value analysis, pointer analysis and program slicing, to model and analyze resource usage in a program. We have conducted experiments to derive usage bounds of various resources in C programs, including heap memory, file descriptors, sockets, user-defined resources, etc. The result suggests that our approach can infer usage bounds of resources in practical imperative programs.

Linear programming is a key technique for analysis and verification of numerical properties in programs, neural networks, etc. In particular, in program analysis based on abstract interpretation, many numerical abstract domains (such as Template Constraint Matrix, constraint-only polyhedra, etc.) are designed on top of linear programming. However, most state-of-the-art linear programming solvers use floating-point arithmetic in their implementations, leading to an approximate result that may be unsound. On the other hand, the solvers implemented using exact arithmetic are too costly. To this end, this paper focuses on advancing rigorous linear programming techniques based on floating-point arithmetic for building sound and efficient program analysis. Particularly, as a supplement to existing techniques, we present a novel rigorous linear programming technique based on Fourier-Mozkin elimination. On this basis, we implement a tool, namely, RlpSolver, combining our technique with existing techniques to lift effectiveness of rigorous linear programming in the scene of analysis and verification. Experimental results show that our technique is complementary to existing techniques, and their combination (RlpSolver) can achieve a better trade-off between cost and precision via heuristic rules.

It is widely desired to precisely predict bounds of resource usages statically in a program, particularly when the program runs in resource-limited contexts. The resource bound problem becomes more challenging for C programs due to the allowed flexible manipulations on dynamically allocated resources in C. In this paper, we present a static analysis approach to deriving the bounds of dynamically allocated resources for C programs. The key idea is to combine numerical value analysis with pointer analysis under the unified framework of abstract interpretation. First, to track resource usage, we intro-duce auxiliary numerical variables to model the resource usage due to resource-manipulating functions such as allocation and deallocation. Second, to handle resource-manipulating functions involving pointers as parameters or return values, we propose a pointer analysis approach designed specifically for resource bound analysis, and combine it with numerical value analysis, to handle pointer arithmetics, dynamic allocation and deallocation, etc. Then, we infer the value bound of auxiliary resource-usage modeling variables to predict resource bounds at each program location. We have implemented our approach in a tool called DARB and conducted experiments on a set of benchmarks extracted from real-world programs. The results show that DARB can deal with C programs with complex resource manipulations.