We briefly survey the field of computer theorem proving and emphasize the recent interest in using theorem provers for the verification of computer systems. We point out a significant hole in existing practice, where verification of many interesting systems cannot be performed for lack of mathematical infrastructure concerning the real numbers and classical ‘continuous’ mathematics. This motivates the remainder of the book where we show how to plug this gap, and illustrate the possibilities with some applications.
KeywordsPrefix Veri Culmination
Unable to display preview. Download preview PDF.