Event Navigation
Dissertation Information
Title: Leveraging Incrementality Of Data-Flow Program Analysis To Improve Analysis Over Weakly-Relational Abstract Domains
Program: Doctor of Philosophy in Computing
Advisor: Dr. Elena Sherman, Computer Science
Committee Members: Dr. Jim Buffenbarger, Computer Science and Dr. Marion Scheepers, Mathematics
Abstract
Developing correct, defect-free software is an important goal of software engineering. Numerical static analysis is a powerful technique that proves the absence of defects. The technique computes program invariants that are then checked for defects. Numerical static analysis is based on data-flow analysis (DFA) and abstract domain concepts. The role of DFA is to compute invariants, and abstract domains define the invariant expressiveness. The drawback of static analysis is that they can produce false positive results when computed invariants are not precise. In order to improve the invariant precision, a numerical analyzer uses advanced numerical domains, such as weakly-relational domains like Zones or Octagons.
However, running a static analyzer on these domains can be cost-prohibitive for large programs, which impedes the adoption of precise numerical analysis by industry. The source of inefficiencies lies in (1) manipulations of abstract states over large variable spaces and (2) improper choice of computationally expensive abstract domains. To improve efficiency of numerical static analyzers, researchers focus on improving efficiency of abstract domain operations and justifying a choice of a more efficient, but less precise, abstract domain type.
In this dissertation, we investigate these two areas of improvements but in the incremental context of DFA. In particular, we define abstract state operations and abstract state comparison as incremental problems of the DFA’s framework. This dissertation describes, formally proves, and empirically evaluates novel state-of-the-art algorithms that improve the efficiency of numerical analysis up to an order of magnitude on large programs and dramatically increases precision of comparing invariants from different domain types.