-
Définition de raffinement contextuel pour des machines à capacités (en)
Rapport de stage M2, encadré par Lars Birkedal
Mars 2023
Résumé
Contextual refinement is a useful notion to relate two open programs x and y by saying
that for all contexts C, any observable behavior of C[x] is also seen in C[y]. As such it
offers a strong relation based only on the operational semantics of closed programs. I
present here a definition of contextual refinement for capability machines, a type of CPU
which uses special hardware checks to enforce safety constraints on memory accesses. I
explain the challenges of porting refinement to low-level programs, show some results
obtained by combining refinement with capability safety, and explore how refinement can
be proven using a logical binary relation.
-
Développement d'une ALU multiprécision (en)
Rapport de stage M1, encadré par Carl Seger
Juillet 2021
-
Développement d'une chaîne de boot sécurisée
Rapport de stage M1, encadré par Patrice Hameau
Juillet 2020
-
Résolution efficace de systèmes d'équations linéaires à coefficients entiers ou polynomiaux : étude et implémentation
Rapport de stage L3, encadré par Romain Lebreton et Pascal Giorgi
Juillet 2019
-
Résolution efficace de systèmes d'équations linéaires par développement en série
Rapport de mémoire maths-info L3, encadré par Jérémy Berthomieu
Juin 2019
-
Percolation dans un graphe plan
Rapport de TIPE MPI
Juin 2018
-
Codes correcteurs d'erreurs : code de Hamming et Reed-Solomon
Rapport de TIPE MPSI
Juin 2017
-
Mon CV :
-
Notes de cours de classe préparatoire :
MPI - 2ème année
2018
-
Notes de cours de classe préparatoire :
MPSI - 1ère année
2017
