|In this talk, we provide an overview of the building blocks of emerging techniques for reasoning about what a program can do and more importantly what it cannot do, i.e., crash. The roots of these ideas date back thousands of years to the Greek's development of alethic, or temporal, logic which allow one to describe what a system might and must do. These logics saw a revival in the 1970s with the connection to Kripke models (developed by Omaha native Saul Kripke) that can capture the time-varying behavior of systems. In 1980 the flood gates opened in this area when Clarke and Sifakis simultaneously developed a fully automatic procedure for comparing a Kripke model of a system's behavior to a temporal logic description of its intended behavior. The past decade has seen the rapid maturation of automated reasoning tools to the point where Microsoft developers are now using them to build better software.