A path-sensitive static analysis considers each possible execution path through a program separately, potentially yielding much more precise results than an analysis that makes fewer distinctions among paths. While precise path-sensitive reasoning is known to be necessary to prove many interesting facts about programs, fully path-sensitive analyses have not scaled well because standard representations of program paths quickly grow out of control.

In this talk, I will describe two techniques that allow path-sensitive program analyses to scale. I will first introduce on-line constraint simplification, which eliminates redundant subparts of logical formulas used to distinguish execution paths. In practice, the formulas used to describe program paths are highly redundant; thus, techniques for keeping path formulas concise can have a dramatic impact on analysis scalability. A second, complementary technique reduces formula size even further: Because static analyses are typically only interested in answering may (i.e., satisfiability) and must (i.e., validity) queries, I will show how to extract from the original path formulas a pair of satisfiabilty- and validity-preserving formulas that contain many fewer variables and that are as good as the original path formula for answering may and must queries about the program. I will demonstrate that these techniques allow a fully path-sensitive analysis to scale to very large, multi-million line programs for the first time.