Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Fixed-term research position at Mitsubishi Ele...

view this post on Zulip Email Gateway (Jul 03 2021 at 09:26):

From: Florian Faissole <>
Dear all,

Mitsubishi Electric R&D Centre Europe (MERCE) is opening one fixed-term/post-doctoral research position (12 months) in the city of Rennes (France).
The research position focuses on the formal verification of domain-specific floating-point units and the formalization of hardware description languages (VHDL...) using proof assistants.

Recent compilers and architectures generally declare themselves compatible with the IEEE-754 standard. Nonetheless, it has been noticed that some of them may lead to different results for identical floating-point computations. Formal development efforts have been made to increase confidence in floating-point computations. As an example, the Flocq library for the Coq proof assistant provides a formalization of generic floating-point formats.

Our goal is to initiate the Coq development of a whole correct-by-construction domain-specific Floating-Point Unit (FPU). This includes the design of the hardware instructions set, its formal implementation and the verification of its compliance with IEEE-754 high-level properties as formalized in the Flocq library. In order to complete the formalization effort, it would be interesting to investigate the interaction of these hardware instructions with formally-verified compilers. The project scope also includes the verification of lower-level properties of the floating-point-units, e.g. the compliance of the circuits with the floating-point instructions they are intended to execute, taking the inherent parallelism of hardware into account. An approach would be to compare the formalized instructions with RTL/Netlist implementations. Finally, we envision the formal integration of the FPU into a global processor and its verification.

The detailed position and contact information are provided at the following address:

If you are interested or would like to have additional information, do not hesitate to contact us.

Contact for application: Magali BRANCHEREAU (<>)

Contact for further technical enquiry: Florian FAISSOLE (<>) ; Benoît BOYER (<>).
Best regards,
Florian Faissole.

Last updated: Jul 15 2022 at 23:21 UTC