Invited Paper: Formal Verification at Intel (at LICS 2003)

Authors: John Harrison

Abstract

As designs become more complex, formal verification techniques are becoming increasingly important in the hardware industry. Many different methods are used, ranging from propositional tautology checking up to the use of interactive higher-order theorem provers. Our own work is mainly concerned with the formal verification of floating-point mathematical functions. As this paper aims to illustrate, such applications require a rather general mathematical framework and the ability to automate special-purpose proof algorithms in a reliable way. Our work uses the public-domain interactive theorem prover HOL Light, and we claim that this and similar ‘LCF-style’ theorem provers are a good choice for such applications.

BibTeX

  @InProceedings{Harrison-FormalVerificationa,
    author = 	 {John Harrison},
    title = 	 {Formal Verification at Intel},
    booktitle =  {Proceedings of the Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2003)},
    year =	 {2003},
    month =	 {June}, 
    pages =      {45-54},
    location =   {Ottawa, Canada}, 
    note =       {Invited Talk},
    publisher =	 {IEEE Computer Society Press}
  }