Robust Program Analysis
Since every non-trivial decision problem concerning the run-time behavior of programs is undecidable, program analysis algorithms rely on heuristic reasoning techniques that can be brittle and unpredictable. For example, program analyzers may fail to terminate on some inputs, or report false alarms, or return different results for the same input, or suffer from “butterfly effects”, in which small changes to the program’s source code drastically changes the analysis. As Leino and Moskal put it: "tools can understand our programs, but we cannot understand our tools."Robust program analysis is motivated by the principle that changes to a program should have a predictable impact on its analysis. We might imagine that a software developer has a workflow in which they analyze a program, make changes, re-analyze, make changes, and so on---we would like to be able to make formal guarantees about how analysis result may differ between successive variants of the program. That is, we wish to understand a program analysis as an operation that acts not only on programs, but also on relatinships between programs.
I gave a high-level talk on robust program analysis at the Isaac Newton Institute workshop on verified software, which can be found here.
My group's approach to making program analysis robust is built on the foundation of algebraic program analysis.
Related publications
- Shaowei Zhu, Zachary Kincaid: Reflections on Termination of Linear Loops. CAV 2021.
- Shaowei Zhu, Zachary Kincaid: Termination analysis without the tears. PLDI 2021.
- Jake Silverman, Zachary Kincaid: Loop Summarization with Rational Vector Addition Systems. CAV 2019.
- John Cyphert, Jason Breck, Zachary Kincaid, Thomas W. Reps: Refinement of path expressions for static analysis. POPL 2019.
- Zachary Kincaid, Jason Breck, John Cyphert, Thomas W. Reps: Closed forms for numerical loops. POPL 2019.
- Zachary Kincaid: Numerical Invariants via Abstract Machines. SAS 2018.