Master Internship #2: Formal Verification of a Static Analyzer

From February to June 2017, I worked under the supervision of Eva Darulova at the Max Planck Institute for Software Systems (MPI-SWS), in Saarbrücken, Germany. I worked on a static analyser of floating-point programs called Daisy. I extended the formal verification of Daisy, to provide support for mixed-precision floating-point arithmetic. This formal verification consisted in a certificate checker, written in Coq and HOL4.

You can find my report here, and my slides here. This internship lead to a publication in FMCAD'18.