Summary form only given. Static program analysis suffers from a fundamental trade-off between precision and scalability, and the analyses that scale to the largest programs are generally 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, as well as how these improved capabilities might be used in verification of properties of large systems.