Microsofts driver development tool uses something called SLAM[1] to verify device drivers (which are the primary cause of system crashes), which uses Z3 as an S

Microsofts driver development tool uses something called SLAM[1] to verify device drivers (which are the primary cause of system crashes), which uses Z3 as an SMT[2] solver. SLAM basically models the NT kernel and the Win32 API and checks for loads of bugs. [1] http://msdn.microsoft.com/en-us/library/windows/hardware/gg487498.aspx http://msdn.microsoft.com/en-us/library/windows/hardware/gg4... [2] Satisfiability Modulo Theories