Formal Methods in System Design, vol. 22, pp. 143-153, 2003.
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.