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 <F.Faissole@fr.merce.mee.com>
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:

https://www.mitsubishielectric-rce.eu/job/machine-checked-verification-of-domain-specific/

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

Contact for application: Magali BRANCHEREAU (jobs@fr.merce.mee.com<mailto:jobs@fr.merce.mee.com>)

Contact for further technical enquiry: Florian FAISSOLE (f.faissole@fr.merce.mee.com<mailto:f.faissole@fr.merce.mee.com>) ; Benoît BOYER (b.boyer@fr.merce.mee.com<mailto:b.boyer@fr.merce.mee.com>).
Best regards,
Florian Faissole.


Last updated: Sep 28 2021 at 20:18 UTC