Isil and Tom Dillig, Stanford University


Sound, Complete, and Scalable Path-Sensitive Analysis [PLDI 2008]

We present a new, precise technique for fully path- and
context-sensitive program analysis. Our technique exploits two
observations: First, using quantified, recursive formulas, path- and
context-sensitive conditions for many program properties can be
expressed exactly. To compute a closed form solution to such recursive
constraints, we differentiate between observable and unobservable
variables, the latter of which are existentially quantified in our
approach.  Using the insight that unobservable variables can be
eliminated outside a certain scope, our technique computes
satisfiability- and validity-preserving closed-form solutions to the
original recursive constraints. We prove the solution is as precise as
the original system for answering may and must queries as well as
being small in practice, allowing our technique to scale to the entire
Linux kernel, a program with over 6 million lines of code.