Compilers use graph representations of programs in several analysis and transformation tasks.
These include determining the dominance, post dominance and control dependence relationships between program constructs, defining variable liveness and dead code which can be removed, and defining the independence of loop iterations indicating that a loop can be executed concurrently, to name but a few. Many compiler texts, provide a natural language definition of these properties, and a graph traversing code fragment for implementing them. The problem is that natural language definitions are imprecise and code fragments, while more precise, obscure the meaning of the property in a tangle of code. A better solution is to use temporal logic as a formal definition language of these properties and model checking as a method for locating nodes which satisfy them. We can, for example, write a temporal logic formula defining the notion of dead code.