conclusion
key ideas
a form of testing, but exhaustive within scope
rich property language
relational formula good match for Java
can accommodate partial specs
acknowledgments
analysis ideas: Rinard
tool: Schechter, Shlyakhter
SAT solvers: Nelson, Selman, Kautz, Zhang
Moore: 1980-2000, 3 hrs -> 1 sec
Alcoa! Free while supplies last!
http://sdg.lcs.mit.edu/alcoa