Team for Research in
Ubiquitous Secure Technology

Citation
I. Dillig, T. Dillig, A. Aiken. "Sound, Complete and Scalable Path-Sensitive Analysis". Conference on Programming Language Design and Implementation, 270-280, June, 2008.

Abstract
We present a new, precise technique for fully path- and contextsensitive program analysis. Our technique exploits two observations: First, using quantified, recursive formulas, path- and contextsensitive 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 satisfiabilityand 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.

Electronic downloads

• http://theory.stanford.edu/~aiken/publications/papers/pldi08.pdf

• HTML

  I. Dillig, T. Dillig, A. Aiken. <a
  href="http://www.truststc.org/pubs/611.html"
  >Sound, Complete and Scalable Path-Sensitive
  Analysis</a>, Conference on Programming Language
  Design and Implementation, 270-280, June, 2008.

• Plain text

  I. Dillig, T. Dillig, A. Aiken. "Sound, Complete and
  Scalable Path-Sensitive Analysis". Conference on
  Programming Language Design and Implementation, 270-280,
  June, 2008.

• BibTeX

  @inproceedings{DilligDilligAiken08_SoundCompleteScalablePathSensitiveAnalysis,
      author = {I. Dillig and T. Dillig and A. Aiken},
      title = {Sound, Complete and Scalable Path-Sensitive
                Analysis},
      booktitle = {Conference on Programming Language Design and
                Implementation},
      pages = {270-280},
      month = {June},
      year = {2008},
      abstract = {We present a new, precise technique for fully
                path- and contextsensitive program analysis. Our
                technique exploits two observations: First, using
                quantified, recursive formulas, path- and
                contextsensitive 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 satisfiabilityand
                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.},
      URL = {http://www.truststc.org/pubs/611.html}
  }
  

Posted by Jessica Gamble on 18 Mar 2009.
For additional information, see the Publications FAQ or contact webmaster at www truststc org.