Skip to Main content Skip to Navigation
Habilitation à diriger des recherches

Deductive Formal Verification: How To Make Your Floating-Point Programs Behave

Résumé : Ma recherche se situe à la frontière de deux domaines de recherche: d'une part l'arithmétique des ordinateurs (c'est-à-dire la façon dont les ordinateurs calculent) et d'autre part la preuve formelle de programmes. Le fait de rajouter des preuves certifiées par un assistant de preuves aux démonstrations d'algorithmes et de programmes concernant l'arithmétique des ordinateurs et les nombres flottants offre une garantie solide aux programmes numériques critiques.
Document type :
Habilitation à diriger des recherches
Complete list of metadatas

Cited literature [182 references]  Display  Hide  Download

https://hal.inria.fr/tel-01089643
Contributor : Sylvie Boldo <>
Submitted on : Tuesday, December 2, 2014 - 9:38:12 AM
Last modification on : Friday, April 10, 2020 - 2:10:23 AM
Document(s) archivé(s) le : Tuesday, March 3, 2015 - 10:41:13 AM

File

Identifiers

  • HAL Id : tel-01089643, version 1

Collections

Citation

Sylvie Boldo. Deductive Formal Verification: How To Make Your Floating-Point Programs Behave. Computer Arithmetic. Université Paris-Sud, 2014. ⟨tel-01089643⟩

Share

Metrics

Record views

538

Files downloads

1089