Formal verification has the potential to radically change the landscape of software engineering. Will it become integrated into the software engineering process, or will it remain a fringe science? The adoption of the techniques presented in this book is likely to influence the answer to this question. This book describes, in full detail, the cutting edge of software verification, viz., the complete verification of a compiler for almost all of C90. It is not an easy or casual read, but still a profitable investment for the serious student of computer science.