Formal verification of square root algorithms

John Harrison Formal Methods in System Design, vol. 22, pp. 143-153, 2003.

Abstract:

We discuss the formal verification of some low-level mathematical software for the Intel(R) Itanium(R) architecture. A number of important algorithms have been proven correct using the HOL Light theorem prover. After briefly surveying some of our formal verification work, we discuss in more detail the verification of a square root algorithm, which helps to illustrate why some features of HOL Light, in particular programmability, make it especially suitable for these applications.

DVI, PostScript or PDF

Bibtex entry:

@ARTICLE{harrison-sqrt,                                             
        author          = JRH,                                        
        title           = "Formal Verification of Square Root Algorithms",
        journal         = "Formal Methods in Systems Design",                  
        volume          = 22,                
        year            = 2003,                                           
        pages           = "143--153"}