Scalable Program Analysis Using Boolean Satisfiability

Static program analysis has long suffered from a fundamental trade-off between precision and scalability, and today the analyses that scale to the largest programs invariably are not the most precise methods known. This talk describes how recent advances in algorithms for solving instances of Boolean satisfiability (SAT) can be exploited to relax this trade-off, resulting in analyses that are both more precise and more scalable than existing techniques. Two applications are discussed in detail: an analysis to find misuses of locks, and a static memory leak detector. In both cases a SAT-based analysis models program behavior down to the bit level while still scaling to millions of lines of code; both analyses also find more bugs with fewer false positives than previous methods.