• John Harrison
Part of the Distinguished Dissertations book series (DISTDISS)


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.


Prefix Veri Culmination 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag London Limited 1998

Authors and Affiliations

  • John Harrison
    • 1
  1. 1.New Museums SiteUniversity of Cambridge Computer LaboratoryCambridgeUK

Personalised recommendations