06-04

Nikhil Pimpalkhare will present his FPO "Predictable Inter-Procedural Program Analysis via Almost-Commuting Transition Systems"

Readers: Professors Zachary Kincaid (adviser), Thomas Reps 

Examiners: Aarti Gupta, and Mae Milano, Zachary Kincaid

 

All are welcome to attend.  Abstract follows below.

Program analysis aims to automatically compute properties of programs from their source code. Since the problems that arise are frequently undecidable, the field has largely focused on developing sound analyses that over-approximate the true properties of a program. Modern program analyzers leverage complex heuristics to make these over-approximations as tight as possible, but these heuristics cause brittle performance: minor updates to codebases can cause large unintended swings in analysis precision.

To help tool users anticipate analysis outcomes, a recent line of work has focused on developing analyses that are robust, and in particular \textit{monotone}: if a program is a refinement of another, its analysis should be at least as precise. Monotonicity is a meta-property of the analysis technique; it gives tool users a way to reason about how certain code changes, like refactoring a loop or deleting a variable, will affect their analysis results, without requiring knowledge of the tool's internal mechanisms. However, development on monotone program analysis had been largely confined to the intra-procedural setting (to analyzing procedures without procedure calls).

This thesis develops a framework for designing monotone inter-procedural program analysis. The key idea is to connect context-free reachability results for abstract machines to program analysis via abstract interpretation: we compute the best abstraction of a program within a given model---its reflection---then exactly characterize the input-output behavior of that abstraction. We instantiate this recipe with vector addition systems with resets (VASR), a numerical computational model, establishing techniques to compute the VASR reflection of a program and the context-free reachability relation of VASR. We extend these results to Lossy VASR, a more expressive variant, producing a program analysis tool which is competitive with the state-of-the-art in verification capabilities while providing formal robustness guarantees. We further investigate Semi-Linear VASR, showing that their reachability relation can be computed in polynomial time despite exponential abstraction size. Finally, we unify the reachability results across all three classes under almost-commuting transition systems, (ACTS), algebraically characterizing properties that make these context-free reachability problems tractable. ACTS define a rich frontier of abstraction domains for monotone inter-procedural program analysis.