id: 01979556
dt: a
an: 01979556
au: Sawada, Jun; Gamboa, Ruben
ti: Mechanical verification of a square root algorithm using Taylor’s
    theorem.
so: Aagaard, Mark D. (ed.) et al., Formal methods in computer-aided design. 4th
    international conference, FMCAD 2002, Portland, OR, USA, November 6-8,
    2002. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2517,
    274-291 (2002).
py: 2002
pu: Berlin: Springer
la: EN
cc: I.2.3
ut: 
ci: 
li: http://link.springer.de/link/service/series/0558/bibs/2517/25170274.htm
ab: Summary: The IBM Power4 processor uses Chebyshev polynomials to calculate
    square root. We formally verified the correctness of this algorithm
    using the ACL2(r) theorem prover. The proof requires the analysis on
    the approximation error of Chebyshev polynomials. This is done by
    proving Taylor’s theorem, and then analyzing the Chebyshev polynomial
    using Taylor polynomials. Taylor’s theorem is proven by way of
    non-standard analysis, as implemented in ACL2(r). Since a Taylor
    polynomial has less accuracy than the Chebyshev polynomial of the same
    degree, we used hundreds of Taylor polynomial generated by ACL2(r) to
    evaluate the error of a Chebyshev polynomial.
rv: