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.
KeywordsModel Check Theorem Prove Computer Algebra System High Order Logic Denotational Semantic
Unable to display preview. Download preview PDF.