PhD in Software Verification prepared at
This page is dedicated to the work I have done during my PhD.
Thesis title: Termination Analysis of Floating-Point Programs.
Advisors: Frédéric Mesnard and Étienne Payet.
Keywords: Software Verification, Static Analysis, Termination, Floating-Point Numbers.
Started on: December 2014.
Defended on: December 8, 2017.
Reports: from Amir Ben-Amram (pdf), Sylvie Boldo (pdf), Salvador Lucas (pdf) and the defense jury (pdf).
Mark spent three hours taking a selfie. Now he wants to post it on
Facebook. In order to get as much Likes as possible, he decides to
edit it. He chooses to use ImageMagick1 which is a
command-line tool for image processing. He tries to modify the hue of
the image and then, disaster! ImageMagick stops responding. The culprit
is a software bug that I discovered: the computation of the new
floating-point value of the hue may fail to terminate2.
To the fictional character Mark, that bug is actually not very harmful. His Facebook fans just need to wait a little bit longer until he manages to retouch his selfie. However, there were cases in history where termination bugs and incorrect floating-point computations lead to dramatic events. On one hand, a non-expected infinite loop caused the Microsoft Azure Storage Service to be interrupted for more than ten hours in 20143. On the other hand, a faulty implementation of the floating-point division operation ultimately cost $475 million to Intel in 19944.
This thesis was born from these issues: it is concerned with termination analysis of programs that perform floating-point computations.
Back then, when my PhD completely beat me at the end of the day, this was what comforted me.
And this is something I achieved by the greatest fluke, like how I ended up becoming a scientist (?); sadly I was in night-wear whence the B/W effect.