Un mécanisme de preuve par réflexion pour Why3 et son application aux algorithmes de GMP

Raphaël Rieu-Helft 1, 2
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Complete list of metadatas

https://hal.inria.fr/hal-01943010
Contributor : Raphaël Rieu-Helft <>
Submitted on : Monday, December 3, 2018 - 3:32:17 PM
Last modification on : Friday, May 10, 2019 - 12:24:00 PM
Long-term archiving on : Monday, March 4, 2019 - 3:16:07 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01943010, version 1

Citation

Raphaël Rieu-Helft. Un mécanisme de preuve par réflexion pour Why3 et son application aux algorithmes de GMP. JFLA 2019 - 30èmes Journées Francophones des Langages Applicatifs, Jan 2019, Rousses, France. ⟨hal-01943010⟩

Share

Metrics

Record views

116

Files downloads

188