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.
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.
