« Coots and Swans on the Kennet | Main | The Adventure of English by Melvyn Bragg »

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!


Reader Comments

There are no comments for this journal entry. To create a new comment, use the form below.

PostPost a New Comment

Enter your information below to add a new comment.
Author Email (optional):
Author URL (optional):
All HTML will be escaped. Hyperlinks will be created for URLs automatically.