Scalable Program Analysis Using Boolean Satisfiability
Speaker: Prof. Alex Aiken , Stanford University
Date: February 8 2005
Time: 1:30PM to 3:00PM
Location: CSAIL Star Seminar Room (32-D463)
Host: Hosts: Daniel Jackson and Martin Rinard, CSAIL
Contact: Maria Rebelo, 3-5895, mr@csail.mit.edu
Relevant URL: 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.
URL: http://theory.stanford.edu/~aiken
---
Alex Aiken received his Bachelors degree in Computer Science and Music
from Bowling Green State University in 1983 and his Ph.D. from Cornell
University in 1988. Alex was a Research Staff Member at the IBM Almaden
Research Center (1988-1993) and a Professor in the EECS department at UC
Berkeley (1993-2003) before joining the Stanford faculty in 2003.
See other events that are part of
See other events happening in February 2005
