Thursday, October 26, 2006
4:15 pm
B17 Upson Hall

Computer Science
Fall 2006

Alex Aiken
Stanford University

Scalable Program Analysis Using Boolean Satisfiability

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.