| 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. |