Enhancing Algebraic Program Analysis

Abstract

Many programs have important functional-correctness properties that involve sophisticated mathematical relationships between numerical variables. Additionally, many programs have important numerical properties that characterize their worst-case usage of resources, such as time or memory. This dissertation applies a framework called algebraic program analysis to the problem of proving numerical properties of programs. In this framework, the main steps of the analysis of a program are encapsulated by an algebraic structure (i.e., a carrier set and a collection of operations), and results are obtained by evaluating expressions that are constructed from the operations of that structure. More specifically, this dissertation explores three enhancements of Compositional Recurrence Analysis (CRA), which is an instance of algebraic program analysis in which the loops of a program are analyzed by finding and solving recurrence relations.

The first enhancement is an interprocedural version of CRA, which we call ICRA. ICRA applies recurrence-solving in a uniform way to both (i) loops, and (ii) linearly recursive procedures, i.e., procedures that make at most one recursive call along any path through the procedure body. The second enhancement improves ICRA's analysis of non-linear mathematical relationships, allowing it to find invariants that include polynomials, exponentials, and logarithms. One component of this enhancement is a new recurrence solver based on the operational calculus; another component is a new abstract domain called the wedge abstract domain, which provides some support for reasoning about non-linear arithmetic. The third enhancement improves ICRA's ability to analyze non-linearly recursive procedures, such as divide-and-conquer algorithms. This enhancement combines two streams of ideas from the literature on generating numerical invariants, namely: (1) template-based methods, and (2) recurrence-based methods. The new analysis technique uses a new kind of template in which the unknowns are functions, and the analyzer finds and solves recurrence constraints on those unknowns. Experiments show that the enhanced analysis is effective at proving assertions and finding resource-usage bounds. For instance, it is able to show that (i) the time taken by merge-sort is O(n log(n)), and (ii) the time taken by Strassen's algorithm is O(n^log_2(7)).