Constraint-Based Analysis in the Presence of Uncertainty and Imprecision

February 19, 2009
Isil Dillig and Thomas Dillig | Stanford University

In all sound program analysis systems there is some mechanism for modeling non-deterministic choice, which is typically used to correctly capture effects of the program’s environment (Did malloc return a valid pointer or null? Which thread did the scheduler pick?) and imprecision in the analysis (Which element was read by the array reference? Is a certain key in the hash map?). In constraint-based analyses it is common to model such decisions as an unconstrained variable ranging over the possible outcomes (e.g., malloc returned either null or a pointer, but not both). Unfortunately, this very useful idea leads to both theoretical and practical difficulties. On the theoretical side, each choice should introduce a fresh variable, leading to a potentially unbounded number of variables in recursive procedures; practically, even in relatively small, non-recursive problems the number of such variables imposes real limits on scalability.

In this talk we present a solution to both the theoretical and practical problems. Given a (recursive) formula F with variables representing non-deterministic choices, we eliminate such variables in favor of two formulas capturing upper and lower bounds on F: the strongest necessary and weakest sufficient conditions under which the original formula was satisfiable and valid, respectively. These formulas are satisfiable/valid exactly when F is, so there is no loss of information in the transformation, and in practice these formulas are much smaller than F. We apply this idea to SAT-based path- and context-sensitive program analysis and demonstrate the practicality of the approach by analyzing programs as large as the entire Linux kernel.

Speaker Details

Isil Dillig is a third year computer science PhD student at Stanford University working with Alex Aiken. She received her BS in computer science from Stanford University in 2006. Her research interests include program analysis and verification and decision procedures.

Thomas Dillig is a third-year PhD student at Stanford University, working with Alex Aiken. He was formerly a member of the SATURN project and is currently working on program analysis as well as constraint solving.