About four years ago David Luckham hinted to me the possibility of verifying
a "real" compiler. At that time the idea seemed unrealistic, even absurd. After
looking closer at the problem and getting more familiar with the possibilities of
the Stanford verifier a verified compiler appeared not so impossible after all. In
fact, I was fascinated by the prospect of creating a large, correct piece of software;
so this subject became my thesis topic. I am very grateful to David Luckham for
suggesting this topic and for his continued advice.
The research has drastically changed my view of verification and programming
in general. Analysis and design of programs (even large ones) can be subject to
rigorous mathematical treatment - the art of programming may become a science
after all. Naturally, the reader will be skeptical, still, I hope to be able to convey
some of my fascination.
This text is a revised version of my Ph.D. thesis. The research was done at
Stanford University and was supported by the Advanced Research Projects Agency
of the Department of Defense, by the National Science Foundation, and by the
Studienstiftung des dcutschen Volkes.
This work would have been impossible without the use of the Stanford verifier.
I have to thank all members of the Stanford verification group for providing this
excellent tool. Don Knuth's text processing system TEX was a most valuable asset
for typesetting a manuscript that must be any typist's nightmare.
I would like to thank my thesis committee David Luckham, Zohar Manna, and
Susan Owicki for their valuable time, for their careful reading, and for their helpful
advice. Friedrich von Hcnkc contributed through numerous discussions and careful
perusal of initial drafts of my writing. Bob Boyer, J Moore, Bob Tennent, and Brian
Wichman provided valuable comments on the original thesis which have improved
the present text. Last but not least I thank my wife Gudrun for her patience and
support.
