2 Search Results for "Jeannerod, Claude-Pierre"

Document
DOI: 10.4230/LIPIcs.ITP.2024.14
End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation

Authors: Florian Faissole, Paul Geneau de Lamarlière, and Guillaume Melquiond

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
Designing an efficient yet accurate floating-point approximation of a mathematical function is an intricate and error-prone process. This warrants the use of formal methods, especially formal proof, to achieve some degree of confidence in the implementation. Unfortunately, the lack of automation or its poor interplay with the more manual parts of the proof makes it way too costly in practice. This article revisits the issue by proposing a methodology and some dedicated automation, and applies them to the use case of a faithful binary64 approximation of exponential. The peculiarity of this use case is that the target of the formal verification is not a simple modeling of an external code; it is an actual floating-point function defined in the logic of the Coq proof assistant, which is thus usable inside proofs once its correctness has been fully verified. This function presents all the attributes of a state-of-the-art implementation: bit-level manipulations, large tables of constants, obscure floating-point transformations, exceptional values, etc. This function has been integrated into the proof strategies of the CoqInterval library, bringing a 20× speedup with respect to the previous implementation.
Cite as

Florian Faissole, Paul Geneau de Lamarlière, and Guillaume Melquiond. End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{faissole_et_al:LIPIcs.ITP.2024.14,
  author =	{Faissole, Florian and Geneau de Lamarli\`{e}re, Paul and Melquiond, Guillaume},
  title =	{{End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.14},
  URN =		{urn:nbn:de:0030-drops-207420},
  doi =		{10.4230/LIPIcs.ITP.2024.14},
  annote =	{Keywords: Program verification, floating-point arithmetic, formal proof, automated reasoning, mathematical library}
}
Document
DOI: 10.4230/DagSemProc.06271.16
Using fast matrix multiplication to solve structured linear systems

Authors: Eric Schost, Alin Bostan, and Claude-Pierre Jeannerod

Published in: Dagstuhl Seminar Proceedings, Volume 6271, Challenges in Symbolic Computation Software (2006)

Abstract
Structured linear algebra techniques are a versatile set of tools; they enable one to deal at once with various types of matrices, with features such as Toeplitz-, Hankel-, Vandermonde- or Cauchy-likeness. Following Kailath, Kung and Morf (1979), the usual way of measuring to what extent a matrix possesses one such structure is through its displacement rank, that is, the rank of its image through a suitable displacement operator. Then, for the families of matrices given above, the results of Bitmead-Anderson, Morf, Kaltofen, Gohberg-Olshevsky, Pan (among others) provide algorithm of complexity $O(alpha^2 n)$, up to logarithmic factors, where $n$ is the matrix size and $alpha$ its displacement rank. We show that for Toeplitz- Vandermonde-like matrices, this cost can be reduced to $O(alpha^(omega-1) n)$, where $omega$ is an exponent for linear algebra. We present consequences for Hermite-Pad'e approximation and bivariate interpolation.
Cite as

Eric Schost, Alin Bostan, and Claude-Pierre Jeannerod. Using fast matrix multiplication to solve structured linear systems. In Challenges in Symbolic Computation Software. Dagstuhl Seminar Proceedings, Volume 6271, pp. 1-5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{schost_et_al:DagSemProc.06271.16,
  author =	{Schost, Eric and Bostan, Alin and Jeannerod, Claude-Pierre},
  title =	{{Using fast matrix multiplication to solve structured linear systems}},
  booktitle =	{Challenges in Symbolic Computation Software},
  pages =	{1--5},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6271},
  editor =	{Wolfram Decker and Mike Dewar and Erich Kaltofen and Stephen Watt},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06271.16},
  URN =		{urn:nbn:de:0030-drops-7787},
  doi =		{10.4230/DagSemProc.06271.16},
  annote =	{Keywords: Structured matrices, matrix multiplication, Hermite-Pade, bivariate interpolation}
}
  • Refine by Author
  • 1 Bostan, Alin
  • 1 Faissole, Florian
  • 1 Geneau de Lamarlière, Paul
  • 1 Jeannerod, Claude-Pierre
  • 1 Melquiond, Guillaume
  • Show More...

  • Refine by Classification
  • 1 Mathematics of computing → Interval arithmetic
  • 1 Mathematics of computing → Mathematical software performance
  • 1 Software and its engineering → Formal software verification
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Interactive proof systems

  • Refine by Keyword
  • 1 Hermite-Pade
  • 1 Program verification
  • 1 Structured matrices
  • 1 automated reasoning
  • 1 bivariate interpolation
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2006
  • 1 2024

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact