— Roméo La Spina —

PhD Student in Computer Science

2021-2022

M2 MPRI (Master Parisien pour la Recherche en Informatique, second year of Master's degree) as part of the magistère Informatique of the ENS Rennes.

Followed courses:

• 2-04

— Functional programming and type systems (Didier Rémy, François Pottier, Gabriel Scherer, Pierre-Evariste Dagand, Jacques-Henri Jourdan)

• 2-06

— Abstract interpretation: application to verification and static analysis (Antoine Miné, Jérôme Feret, Xavier Rival, Caterina Urban)

• 2-07-1

— Foundations of proof systems (Benjamin Werner)

• 2-07-2

— Proof assistants (Bruno Barras, Matthieu Sozeau)

• 2-18-1

— Distributed algorithms on networks (Pierre Fraignaud, Ami Paz, Mikaël Rabie)

• 2-18-2

— Distributed algorithms on shared memory (Carole Delporte, Hugues Fauconnier)

• 2-23-1

— Synchronous systems (Marc Pouzet, Timothy Bourke)

• 2-30

— Proofs of security protocols (Bruno Blanchet, Hubert Comon, Vincent Cheval, Adrien Koutsos)

• 2-36-1

— Proofs of programs (Claude Marché, Jean-Marie Madiot)

• 2-37-1

— Programming shared memory multicore machines (Luc Maranget, Adrien Guatto)

M2 Research Internship

Subject: A data-flow analyser parametrized by an iteration order for the formally verified compiler CompCert [detailed subject] [Report, slides (in French)]
Supervisors: Sandrine Blazy, Delphine Demange (IRISA, Rennes, CELTIQUE/EPICURE team)

2020-2021

M1 SIF (Science Informatique, first year of Master's degree), co-managed by the Université Rennes 1 and the ENS Rennes.

Detailed description of the followed courses

M1 Research Internship

Sujet: Secure compilation of speculative-constant-time programs [Slides]
Supervisor: Vincent Laporte (LORIA, Nancy, PESTO team)

Research Project

Subject: Verification of a Just-In-Time compiler [Report]
Supervisors: David Pichardie, Aurèle Barrière (IRISA, Rennes, CELTIQUE team)

2019-2020

L3 Informatique Fondamentale (third year of Bachelor's degree), co-managed by the Université Claude Bernard Lyon 1 and the ENS de Lyon.
Admission to the Master's degree cycle (concours cycle master) in computer science at the ENS Rennes.

Detailed description of the followed courses

L3 Research Internship

Subject : Study of the scalability of video conference servers [Report, slides (in French)]
Supervisor : Gilles Muller (INRIA Paris, WHISPER team)