-
Defining contextual refinement for capability machines
Internship Report M2, supevised by Lars Birkedal
March 2023
Abstract
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.
-
Developing a multiprécision ALU
Internship Report M1, supevised by Carl Seger
July 2021
-
Secure bootloader development
Internship Report M1, supevised by Patrice Hameau
July 2020
-
Efficient resolution of linear systems with integer or polynomial coefficients: study and implementation (fr)
Internship Report L3, supevised by Romain Lebreton and Pascal Giorgi
July 2019
-
Efficient resolution of linear systems by series expansion (fr)
Research report L3, supervised by Jérémy Berthomieu
June 2019
-
Percolation in a planar graph (fr)
TIPE Report MPI
June 2018
-
Error correction codes: Hamming and Reed-Solomon
TIPE Report MPSI
June 2017
