Sound Floating-point And Non-convex Static Analysis Using Interval Linear Abstract Domains

Trustworthiness of software has become the center of attention when consider-ing modern software quality. Finding bugs before release is fundamental to buildtrustworthy software, which is extremely important for safety-critical applicationssuch as aerospace, defense and automotive. Scienti?c and engineering programs es-pecially safety-critical embedded software are usually related to mathematics andphysics, and thus often involve a lot of numerical computations. Hence, many pro-gram bugs including division by zero, arithmetic over?ows and array out-of-bounds,are closely related to numerical properties in the program.Abstract interpretation is a theory of semantics approximation, allowing thedesign of sound and e?cient static analyses. Abstract domains are a key ingredi-ent in this framework: They enable semantic choices (what properties to infer) andalgorithmic choices (how to compute). In this thesis, we focus on design and im-plementation of numerical abstract domains that are used to automatically discovernumerical properties over program variables. Over the past decades, a wide variety ofnumerical abstract domains have been proposed. However, most existing abstractdomains (especially relational ones) need arbitrary precision rational numbers tobuild implementations, which may degrade the time and memory e?ciency. Mostof them can only represent convex properties, and hence have limitations in deal-ing with disjunctions. Besides, currently there is no abstract domain that supportsinterval variable coe?cients which appear naturally in real-life program analysis.The goal of this thesis is to explore more e?cient numerical abstract domains,using sound ?oating-point constructions, and to design more precise ones, allowingnon-convex properties and interval coe?cients.Major contributions of this thesis are listed as follows.1) We present a so-called ?oating-point polyhedra abstract domain. The clas-sical convex polyhedra domain is one of the most powerful and commonly used ab-stract domains in the ?eld, but rational implementations may su?er from scalabilityproblems. To solve this issue, we present an implementation using ?oating-pointarithmetic without sacri?cing soundness, based on a constraint-only representation using ?oating-point coe?cients. Since its complexity mainly comes from the costlyjoin operation (i.e., polyhedral convex hull), a series of cheap weak join operationsare then proposed.2) We introduce interval linear algebra to static analysis and propose intervallinear abstract domains that support interval coe?cients. Intervals are naturallysuited to construct sound ?oating-point abstract domains. First, a so-called intervalpolyhedra domain is proposed to infer interval linear inequalities. Then, a restrictedabstract domain is proposed based on a system of interval linear equalities in rowechelon form, polynomial in time and memory. The two domains can be consid-ered as interval extensions of the existing convex polyhedra domain and the a?neequality domain respectively. By interpreting solutions as weak solutions of intervallinear systems, both domains can express certain non-convex (even unconnected)properties. They are soundly implemented using ?oating-point numbers based oninterval arithmetic with outward rounding.3) We present linear absolute value abstract domains that natively allow toexpress non-convex properties. Absolute value (AV) is fundamental in mathematicsand often used to describe piecewise linear behavior. The equivalence among linearAV inequality systems, interval linear inequality systems and extended linear com-plementarity problem (XLCP) systems is stated. We construct a double descriptionmethod for XLCP on top of that for polyhedra, based on which a new method forsolving AV linear programming problems is shown. On this basis, we propose anabstract domain of linear AV equalities, and an abstract domain of linear AV in-equalities that has the same expressiveness as interval polyhedra domain but enjoysoptimal transfer functions. They are implemented using rational numbers based onthe double description method for XLCP.The numerical abstract domains presented in this thesis provide di?erent trade-o?s between precision and e?ciency, and can be applied to di?erent problems. Theyare implemented in the APRON library, and experimental results are encouraging.