Generating formally certified bounds on values and round-off errors.
Résumé
We present a new tool that generates bounds on the values and the round-off errors of programs using floating point operations. The tool is based on forward error analysis and interval arithmetic. The novelty of our tool is that it produces a formal proof of the bounds that can be checked independently using an automatic proof checker such as Coq and a complete model of floating point arithmetic. For the first time ever, we can easily certify that simple numerical programs such as the ones usually found in real time applications do not overflow and that round-off errors are below acceptable thresholds. Such level of quality should be compulsory on safety critical applications. As our tool is easy to handle, it could also be used for many pieces of software.
Nous présentons un nouvel outil capable de générer, à partir de la description d'un programme qui utilise des opérations à virgule flottante, des bornes sur les valeurs des variables et les erreurs d'arrondi commises dans le programme. L'outil est basé sur l'analyse d'erreur en mode direct et l'arithmétique d'intervalles. La nouveauté de l'outil est qu'il produit une preuve formelle des bornes qui peut être certifié indépendamment en utilisant un outil automatique de preuve tel que Coq et un modèle complet de l'arithmétique à virgule flottante. Pour la première fois, il es possible de facilement certifier que les programmes numériques simples comme ceux habituellement utilisés dans les applications en temps réel ne commettent pas de dépassement de capacité et que les erreurs d'arrondi sont au_dessous de seuil acceptables. Un tel niveau de qualité devrait être obligatoire sur les applications critiques. Comme notre outils est facile à manipuler, ce niveau devrait également être utilisé pour de nombreux logiciels.
| Origine | Fichiers produits par l'(les) auteur(s) |
|---|