The purpose of program analysis is to over-approximate the run-time behavior of programs. The classical method for analyzing programs is iterative program analysis, in which one begins with some property that over-approximates (just) the initial states of the program, and repeatedly transforms the property until converging upon a property that over-approximates all of the reachable states of the program. An alternative to iterative program analysis is algebraic program analysis, in which the space of program properties forms an algebraic structure, and one computes a property that over-approximates the executions of a program by breaking it into smaller parts, analyzing each part, and then using the operations of the algebraic structure to combine the results into a property that over-approximates the execution of the whole program. The purpose of this tutorial is to provide an introduction to algebraic program analysis, and teach participants how to design program analyses in the algebraic style. The first part of the tutorial will introduce the algebraic framework, following Tarjan’s path-expression method for intraprocedural analysis. We will motivate algebraic program analysis with compositional recurrence analysis, which computes numerical loop invariants over an expressive abstract domain without requiring a widening operator. The second part of the tutorial will cover recent work on interprocedural algebraic program analysis. We will focus on a family of techniques that take inspiration from Newton’s method for finding roots of real-valued functions to compute solutions to interprocedural program-analysis problems.
Mon 8 Jan
|14:00 - 15:30|