Termination Analysis of Floating-Point Computations

Le tristement célèbre Ecran Bleu de la Mort de Windows introduit bien le problème traité. Ce bug est souvent causé par la non-terminaison d'un pilote matériel : le programme s'exécute infiniment, bloquant ainsi toutes les ressources qu'il s'est approprié pour effectuer ses calculs. Cette thèse développe des techniques qui permettent de décider, préalablement à l'exécution, la terminaison d'un programme donné pour l'ensemble des valeurs possibles de ses paramètres en entrée. En particulier, nous nous intéressons aux programmes qui manipulent des nombres flottants. Ces nombres sont omniprésents dans les processeurs actuels et sont utilisés par pratiquement tous les développeurs informatiques. Pourtant, ils sont souvent mal compris et, de fait, source de bugs. En effet, les calculs flottants sont entachés d'erreurs, inhérentes au fait qu'ils sont effectués avec une mémoire finie. Par exemple, bien que vraie dans les réels, l'égalité 0.2 + 0.3 = 0.5 est fausse dans les flottants. Non gérées correctement, ces erreurs peuvent amener à des évènements catastrophiques, tel l'incident du missile Patriot qui a fait 28 morts. Les théories que nous développons sont illustrées, et mises à l'épreuve par des extraits de codes issus de programmes largement répandus. Notamment, nous avons pu exhiber des bugs de terminaisons dues à des calculs flottants incorrects dans certains paquets de la distribution Ubuntu.The infamous Blue Screen of Death of Windows appropriately introduces the problem at hand. This bug is often caused by a non-terminating device driver: the program runs infinitely, blocking in the process all the resources it allocated for its calculations. This thesis develops techniques that allow to decide, before runtime,termination of a given program for any possible value ​​of its inputs. In particular, we are interested in programs that manipulate floating-point numbers. These numbers are ubiquitous in current processors andare used by nearly all software developers. Yet, they are often misunderstood and, hence, source of bugs.Indeed, floating-point computations are tainted with errors. This is because they are performed within a finite amount of memory. For example, although true in the reals, the equality 0.2 + 0.3 = 0.5 is false in the floats. Not handled properly, these errors can lead to catastrophic events,such as the Patriot missile incident that killed 28 people. The theories we develop are illustrated, and put to the test, by code snippets taken from widely used programs. Notably, we were able to exhibit termination bugs due toincorrect floating-point computations in some packages of the Ubuntu distribution