Skip to main content
18 votes

How can I prove facts about floating point calculations?

I recommend the monograph Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System by Sylvie Boldo and Guillaume Melquiond. It addresses your questions and much, ...
Andrej Bauer's user avatar
  • 9,593
7 votes
Accepted

PDEs and proof assistants

Have you seen the updates from more recent work of the same Coq group you cite? To quote from their article this week: Our long-term purpose is to formally prove the correctness of parts of a library ...
macbeth's user avatar
  • 394
7 votes

PDEs and proof assistants

A fragment of traditional PDE theory has been formalized in Mizar: Sora Otsuki and Pauline N. Kawamoto and Hiroshi Yamazaki, "A Simple Example for Linear Partial Differential Equations and Its ...
Alex Nelson's user avatar
  • 1,574
6 votes

Tools to check correctness of decimal floating point arithmetic

If you have implemented "a library of functions that evaluate basic arithmetic, as well as some transcendental functions such as cosine, on decimal floating point numbers" and you want to ...
Nike Dattani's user avatar
  • 1,165
4 votes

How can I prove facts about floating point calculations?

The HOL4 formalisations of floating point numbers define them as a record type: float = <| Sign : word1; Exponent : 'w word; Significand : 't word |> where ...
Michael Norrish's user avatar
2 votes

PDEs and proof assistants

To add to the list in the question and the answers, recently I came across a couple of papers by another research group working towards the formalization/verification of the relevant numerical ...
user9716869 - supports Ukraine's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible