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 | Site Map | Site powered by SPIP 3.1.15 + AHUNTSIC [CC License]

info visites 1819108