A self-contained introduction for anyone familiar with the fundamentals of the theory of machines. The book is well indexed and contains a substantial bibliography, as well as pointing to the implementation of the verification techniques in the COSPAN system. --Computing Reviews