verified decomposition of arithmetic operators

Depending on the processor, certain arithmetic operations may be implemented natively or by composition of elementary operations. Our goal is to formally verify some such decompositions.

The goal of the internship is to deepen existing work done within the group to be able to prove some expansions of arithmetic operators correct within the CompCert verified compiler.


Contact | Plan du site | Site réalisé avec SPIP 4.2.16 + AHUNTSIC [CC License]

info visites 4184936