SMT solvers have been the focus of increased recent attention 
thanks to technological advances and an increasing number of 
applications. The Z3 solver from Microsoft Research is noteworthy
both concerning technological advances and applications. I will describe 
several of the applications of Z3, such Pex (Program EXploration) for 
generating test cases for .NET binaries, SAGE for security testing, 
Static Driver Verifier version 2.0 (shipped with the Windows 7 Driver 
Development Kit), PREfix (enchanced with bit-precise reasoning to find integer
overflows), SpecExplorer from the Protocol Test Team for generating test inputs
from model-based test suites, as well as the HAVOC and VCC verifiers for C code.