Cross Checking Implementations for Bugs

Placeholder Show Content



Using static analysis to analyze large source bases for errors can be difficult because the correctness rules in the system are often numerous and undocumented. In order to check those systems, a human would have to enumerate those rules at the cost of weeks or years of effort. Engler et. al [7] introduced techniques to infer many of those rules from the source itself, saving much of the human effort. This thesis leverages some of those techniques to cross check implementations for consistency.
If there are multiple implementations of the same interface (i.e. device drivers all implement open, close, read, write), we can analyze the actions of those implementations to infer the correct behavior. For example, if most of the implementations check the first argument of open for NULL before dereferencing it, it is likely that all of the implementations should check that argument for NULL before dereferencing it. The implementations missing the checks are assumed to be in error.
To demonstrate the flexibility and capability of our technique, we use static analysis to infer the rules for four classes of bugs and apply them to the Linux kernel. We found dozens of errors with relatively little user effort in spite of the kernel's size and lack of documentation.


Type of resource text
Date created 2004-05


Author Ashcraft, Kenneth
Advisor Engler, Dawson
Advisor Shoham, Yoav
Department Stanford University. Department of Computer Science.


Subject Computer software > Testing
Subject Debugging in computer science
Genre Thesis

Bibliographic information

Access conditions

Use and reproduction
User agrees that, where applicable, content will not be used to identify or to otherwise infringe the privacy or confidentiality rights of individuals. Content distributed via the Stanford Digital Repository may be subject to additional license and use restrictions applied by the depositor.
This work is licensed under a Creative Commons Attribution Non Commercial 3.0 Unported license (CC BY-NC).

Preferred citation

Preferred Citation
Ashcraft, Kenneth (2004). Cross Checking Implementations for Bugs. Stanford Digital Repository. Available at


Undergraduate Theses, School of Engineering

View other items in this collection in SearchWorks

Contact information

Also listed in

Loading usage metrics...