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.
Is the existence of polyhedral inductive invariants decidable?
Global value numbering is kind of program optimization. How can we certify it formally at reasonable cost in both formalization and compilation time ?
Counter-measures against hardware control-flow attacks, speculative execution attacks, or side channel attacks are notoriously difficult to insert at the source level. The topic of this internship is to inject them at compile-time.
Hash-consing is a very useful technique for implementing certain kinds of algorithms, particularly in program analysis, logic, symbolic computation. Since it is very imperative, it is difficult to formalize in a purely functional setting. The goal of the internship is to apply new approaches to achieve this goal.
The goal of the proposed research is to provide a decision procedure for the Coq proof assistant that would extend equality-based reasoning (i.e. the congruence tactic) to heterogeneous problems where equalities are expressed using multiple equivalence relations (i.e. setoids).