Algebraic Program Analysis

A program analysis is compositional when the result of analyzing a composite program is a function of the results of analyzing its components. Compositionality enables program analyses to scale to large programs, to be parallelized, to be applied incrementally, and to be applied to incomplete programs. Algebraic program analysis is a framework for understanding compositional program analysis through the lens of abstract algebra. We think of a program analysis as an algebraic structure wherein the elements represent summaries of program dynamics, and the operations give means to compose these summaries.

Thomas Reps and I gave a tutorial on algebraic program analysis at CAV 2021, which can be found here.
Algebraic program analysis also serves as the foundation of an approach to robust program analysis---in particular, we can understand how an algebraic analysis will react to certain program transformations in terms of equational laws that are valid in the algebra.

Related publications

Algebraic program analysis frameworks

Algebraic analyses

This project is supported by ONR grant N00014-19-1-2318.