How to avoid proving the absence of integer overflows

Martin Clochard 1, 2 Jean-Christophe Filliâtre 1, 2 Andrei Paskevich 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
Abstract : When proving safety of programs, we must show, in particular, the absence of integer overflows. Unfortunately, there are lots of situations where performing such a proof is extremely difficult, because the appropriate restrictions on function arguments are invasive and may be hard to infer. Yet, in certain cases, we can relax the desired property and only require the absence of overflow during the first n steps of execution, n being large enough for all practical purposes. It turns out that this relaxed property can be easily ensured for large classes of algorithms, so that only a minimal amount of proof is needed, if at all. The idea is to restrict the set of allowed arithmetic operations on the integer values in question, imposing a " speed limit " on their growth. For example, if we repeatedly increment a 64-bit integer, starting from zero, then we will need at least 2 64 steps to reach an overflow; on current hardware, this takes several hundred years. When we do not expect any single execution of our program to run that long, we have effectively proved its safety against overflows of all variables with controlled growth speed. In this paper, we give a formal explanation of this approach, prove its soundness, and show how it is implemented in the context of deductive verification.
Type de document :
Communication dans un congrès
Arie Gurfinkel and Sanjit A. Seshia. 7th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2015, San Francisco, CA, United States. 7th Working Conference on Verified Software: Theories, Tools, and Experiments. 〈http://verifun.eecs.berkeley.edu/vstte15/〉
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01162661
Contributeur : Jean-Christophe Filliâtre <>
Soumis le : vendredi 9 octobre 2015 - 11:16:10
Dernière modification le : vendredi 17 février 2017 - 16:10:44
Document(s) archivé(s) le : mercredi 26 avril 2017 - 22:31:04

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01162661, version 2

Citation

Martin Clochard, Jean-Christophe Filliâtre, Andrei Paskevich. How to avoid proving the absence of integer overflows. Arie Gurfinkel and Sanjit A. Seshia. 7th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2015, San Francisco, CA, United States. 7th Working Conference on Verified Software: Theories, Tools, and Experiments. 〈http://verifun.eecs.berkeley.edu/vstte15/〉. 〈hal-01162661v2〉

Partager

Métriques

Consultations de
la notice

384

Téléchargements du document

142