Home > Topics > Formal Proofs > Jobs and Internships > Jobs and Internships
Jobs and Internships
Masters
- 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.
- (un)decidability of polyhedral invariant inference
Is the existence of polyhedral inductive invariants decidable?
- Verified global value numbering
Global value numbering is kind of program optimization. How can we certify it formally at reasonable cost in both formalization and compilation time ?
- [master] automatic insertion of countermeasures in a verified compiler
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.
- [master] formally verified hash-consing
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.
- [Master] Design and Evaluation of Strategies for Automated Proofs using Reasoning Modulo Equivalence
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).
