Static detection of software errors

This thesis describes three novel static analysis techniques for error detection. First, we present SATURN, a general framework for building precise and scalable analysis for real-world software. SATURN encodes program constructs into boolean constraints and uses a satisfiability solver to infer and check program properties. One key advantage of S ATURN is precision: it is path sensitive, precise down to the bit level, and models pointers and heap data. SATURN is also highly scalable, which we achieve using two techniques. First, several optimizations compress the size of the boolean formulas that model the control- and data-flow and the heap locations accessed by a function. Second, a concise summary is computed for each function, allowing inter-procedural analysis without a dramatic increase in the size of the boolean constraints to be solved. We also present a static analysis algorithm for detecting security vulnerabilities in PHP, a popular server-side scripting language for building web applications. Our analysis employs a novel three-tier architecture to capture information at the intrablock, intraprocedural, and interprocedural levels. This architecture enables us to handle dynamic features of scripting languages that have not been adequately modeled by previous techniques. Finally, we present several lightweight checkers for redundant operations in system software based on the belief that programmers generally attempt to perform useful work. Redundant operations violate this belief and are likely errors. We demonstrate that in fact many redundancies signal mistakes as serious as traditional hard errors such as deadlocks, memory leaks, etc. We conduct extensive experiments on open-source software to validate each of these approaches. We demonstrate their practicality and effectiveness by finding hundreds of previously unknown errors, most of which have been reported to and fixed by their developers.