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
- Zachary Kincaid, Thomas W. Reps, John Cyphert: Algebraic Program Analysis. CAV 2021.
- Shaowei Zhu, Zachary Kincaid: Termination analysis without the tears. PLDI 2021.
- Jason Breck, John Cyphert, Zachary Kincaid, Thomas W. Reps: Templates and recurrences: better together. PLDI 2020.
- John Cyphert, Jason Breck, Zachary Kincaid, Thomas W. Reps: Refinement of path expressions for static analysis. POPL 2019.
- Zachary Kincaid: Numerical Invariants via Abstract Machines. SAS 2018.
- Zachary Kincaid, Jason Breck, Ashkan Forouhi Boroujeni, Thomas W. Reps: Compositional recurrence analysis revisited. PLDI 2017.
- Azadeh Farzan, Zachary Kincaid: Compositional Recurrence Analysis. FMCAD 2015.
- Azadeh Farzan, Zachary Kincaid: An Algebraic Framework for Compositional Program Analysis. ArXiV 2013.
Algebraic analyses
- Shaowei Zhu, Zachary Kincaid: Reflections on Termination of Linear Loops. CAV 2021.
- Zachary Kincaid, Jason Breck, John Cyphert, Thomas W. Reps: Closed forms for numerical loops. POPL 2019.
- Jake Silverman, Zachary Kincaid: Loop Summarization with Rational Vector Addition Systems. CAV 2019.
- Zachary Kincaid, John Cyphert, Jason Breck, Thomas W. Reps: Non-linear reasoning for invariant synthesis. POPL 2018.