Description

We propose to investigate on a possible axiomatization for supporting floating point numbers in the VerCors verification tool [1]. Particularly, we would like to support 32 bit floating point for our C language frontend. This will allow us to reason about floating arithmetic, which is present in a big range of industrial cases where C is a pervasive language.

We should follow the IEEE Standard 754 for Binary Floating-Point Arithmetic [2], and we can get inspired by axiomatizations from other verification tools such as why3 [3].

Your tasks in this work will consist on reading and understanding standards for floating point numbers, plus deciding on an appropriate standard to follow in our formal verification tool. You will then have to implement an axiomatization for this standard using the Viper [4] language, which is VerCors backend for separation-logic-based deductive verification.

You will gain knowledge and experience both on the intricate world of floating point numbers representation, and on the engineering of tools for deductive verification as well as their application on industrial cases.

• [1] https://vercors.ewi.utwente.nl
• [2] https://ieeexplore.ieee.org/document/4610935
• [3] http://why3.lri.fr/stdlib/floating_point.html
• [4] http://viper.ethz.ch/tutorial/