Accueil > Axes > Formal Proofs > Emplois et stages > Emplois et stages
Emplois et stages
Masters
- [master/PhD] Formally verified optimizations for safety-critical embedded code
- [Master] Certification of Distributed Self-Stabilizing Algorithms Using Coq
We propose a framework, based on Coq, to (semi-) automatically construct certified proofs of self-stabilizing algorithms called PADEC. The framework imports into Coq the computational model in which the algorithms are designed, formalizes the algorithms themselves and their specifications. Then the algorithms are proved using Coq including safety, convergence. The current development of the framework includes performance studies and complexity proofs but also connection with other formal tools.
- [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).
