Team for Research in
Ubiquitous Secure Technology

Citation
I. Dillig, T. Dillig, A. Aiken. "8. Static Error Detection Using Semantic Inconsistency Inference". Conference on Programming Language Design and Implementation, 435-446, June, 2007.

Abstract
Inconsistency checking is a method for detecting software errors that relies only on examining multiple uses of a value. We propose that inconsistency inference is best understood as a variant of the older and better understood problem of type inference. Using this insight, we describe a precise and formal framework for discovering inconsistency errors. Unlike previous approaches to the problem, our technique for finding inconsistency errors is purely semantic and can deal with complex aliasing and path-sensitive conditions. We have built a null dereference analysis of C programs based on semantic inconsistency inference and have used it to find hundreds of previously unknown null dereference errors in widely used C programs.

Electronic downloads

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

• HTML

  I. Dillig, T. Dillig, A. Aiken. <a
  href="http://www.truststc.org/pubs/613.html"
  >8.	Static Error Detection Using Semantic Inconsistency
  Inference</a>, Conference on Programming Language
  Design and Implementation, 435-446, June, 2007.

• Plain text

  I. Dillig, T. Dillig, A. Aiken. "8.	Static Error
  Detection Using Semantic Inconsistency Inference".
  Conference on Programming Language Design and
  Implementation, 435-446, June, 2007.

• BibTeX

  @inproceedings{DilligDilligAiken07_8StaticErrorDetectionUsingSemanticInconsistencyInference,
      author = {I. Dillig and T. Dillig and A. Aiken},
      title = {8.	Static Error Detection Using Semantic
                Inconsistency Inference},
      booktitle = {Conference on Programming Language Design and
                Implementation},
      pages = {435-446},
      month = {June},
      year = {2007},
      abstract = {Inconsistency checking is a method for detecting
                software errors that relies only on examining
                multiple uses of a value. We propose that
                inconsistency inference is best understood as a
                variant of the older and better understood problem
                of type inference. Using this insight, we describe
                a precise and formal framework for discovering
                inconsistency errors. Unlike previous approaches
                to the problem, our technique for finding
                inconsistency errors is purely semantic and can
                deal with complex aliasing and path-sensitive
                conditions. We have built a null dereference
                analysis of C programs based on semantic
                inconsistency inference and have used it to find
                hundreds of previously unknown null dereference
                errors in widely used C programs.},
      URL = {http://www.truststc.org/pubs/613.html}
  }
  

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