Eric Hehner on Model-Checking

A year or so ago I came across the following passage which nicely highlights the limitations of using model-checking to verify that programs meet their specifications:

There is an approach to program proving that exhaustively tests all inputs, called model-checking. Its advantage over the theory in this book is that it is fully automated. With a clever representation of boolean expressions (see Exercise 6), model-checking currently boasts that it can explore up to about 10^60 states. That is more than the estimated number of atoms in the universe! It is an impressive number until we realize that 10^60 is about 2^200, which means we are talking about 200 bits. That is the state space of six 32-bit variables. To use model-checking on any program with more than six variables requires abstraction; each abstraction requires proof that it preserves the properties of interest, and these proofs are not automatic. To be practical, model-checking must be joined with other methods of proving, such as those in this book. (Eric C. R. Hehner, A Practical Theory of Programming, 2nd ed, 2002)

Incidentally, you can find an online copy of Hehner's ground-breaking book at http://www.cs.toronto.edu/~hehner/aPToP/.  Unfortunately, many people have not yet noticed that the ground has been broken and seem to be busy trampling it flat again!