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

This project is supported by NSF CAREER award 1942537