• Login
    View Item 
    •   MINDS@UW Home
    • MINDS@UW Madison
    • College of Letters and Science, University of Wisconsin–Madison
    • Department of Computer Sciences, UW-Madison
    • CS Technical Reports
    • View Item
    •   MINDS@UW Home
    • MINDS@UW Madison
    • College of Letters and Science, University of Wisconsin–Madison
    • Department of Computer Sciences, UW-Madison
    • CS Technical Reports
    • View Item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    Enhancing Algebraic Program Analysis

    Thumbnail
    File(s)
    TR1863 Jason Breck.pdf (1.640Mb)
    Date
    2020-08-20
    Author
    Breck, Jason
    Metadata
    Show full item record
    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)).
    Subject
    invariant generation
    recurrence relation
    resource bounds
    static analysis
    Permanent Link
    http://digital.library.wisc.edu/1793/80426
    Part of
    • CS Technical Reports

    Contact Us | Send Feedback
     

     

    Browse

    All of MINDS@UWCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

    My Account

    LoginRegister

    Contact Us | Send Feedback