• DocumentCode
    610859
  • Title

    How to Compute the Area of a Triangle: A Formal Revisit

  • Author

    Boldo, S.

  • fYear
    2013
  • fDate
    7-10 April 2013
  • Firstpage
    91
  • Lastpage
    98
  • Abstract
    Mathematical values are usually computed using well-known mathematical formulas without thinking about their accuracy, which may turn awful with particular instances. This is the case for the computation of the area of a triangle. When the triangle is needle-like, the common formula has a very poor accuracy. Kahan proposed in 1986 an algorithm he claimed correct within a few ulps. Goldberg took over this algorithm in 1991 and gave a precise error bound. This article presents a formal proof of this algorithm, an improvement of its error bound and new investigations in case of underflow.
  • Keywords
    algorithm theory; floating point arithmetic; theorem proving; Kahan algorithm; algorithm proof; floating-point arithmetic; mathematical value; triangle area; Accuracy; Algorithm design and analysis; Digital arithmetic; Electronic mail; Error analysis; Libraries; Standards; Coq; floating-point arithmetic; formal proof; triangle; underflow;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Computer Arithmetic (ARITH), 2013 21st IEEE Symposium on
  • Conference_Location
    Austin, TX
  • ISSN
    1063-6889
  • Print_ISBN
    978-1-4673-5644-2
  • Type

    conf

  • DOI
    10.1109/ARITH.2013.29
  • Filename
    6545896