Program Paths Simplified: Scalable Path-Sensitive Analysis without Heuristics
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.
Thomas Dillig is a PhD candidate at Stanford University. Thomas obtained his undergraduate degree in computer science from Stanford University in 2006 with distinction and honors. His main research interests are program verification, programming languages and constraint solving.