Fonenantsoa Maurica

PhD in Software Verification prepared at
the University of Reunion Island, within the Computer Science and Mathematics Lab.

Since February 2018, I am a postdoctoral researcher at
the French Commission for Atomic Energy and Alternative Energies,
within the Software Reliability and Security Lab.

My PhD (thesis and defense slides)

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.
1 https://www.imagemagick.org/
2 https://www.imagemagick.org/discourse-server/viewtopic.php?f=3&t=31506
3 https://azure.microsoft.com/fr-fr/blog/update-on-azure-storage-service-interruption/
4
http://boole.stanford.edu/pub/anapent.pdf

Publications

  • F. Maurica, F. Mesnard and E. Payet. Optimal Approximation for Efficient Termination Analysis of Floating-Point Loops.
    Presented at the 1st IEEE Conference on Next Generation Computing Applications, 2017. Pointe aux Piments, Mauritius Island.
Preprint, Publication
  • F. Maurica, F. Mesnard and E. Payet. On the Linear Ranking Problem for Simple Floating-Point Loops.
    Presented at the 23rd International Static Analysis Symposium, 2016. Edinburgh, UK.
Preprint, Publication
  • F. Maurica, F. Mesnard and E. Payet. Termination Analysis of Floating-Point Programs using Parameterizable Rational Approximations.
    Presented at the 31st ACM Symposium on Applied Computing, 2016. Pisa, Italy.
Preprint, Publication

Misc

Back then, when my PhD completely beat me at the end of the day, this was what comforted me.




--
Contact me.
Page last modified on March 1, 2018.