back to home page
Cătălin Hriţcu
Current Research Group
Carmine Abate
PhD Student at
Inria Paris
since 2018-06:
The Formal Foundations of Secure Compilation
Research Intern at
Inria Paris
, 2017-12 to 2018-05:
Robust Property Preservation for Secure Compilation
[MSc student at
University of Trento
]
Jérémy Thibault
PhD Student at
Inria Paris
since 2018-08:
Secure Compartmentalizing Compilation to a Tagged Architecture
Research Intern at
Inria Paris
2018-02 to 2018-07:
A Trace-based Proof Technique for Secure Compilation
[MSc student at
ENS Rennes
]
Guido Martínez
Co-Supervised PhD Student at
CIFASIS
-
CONICET
Rosario since 2017-04:
Metatheory for Semi-Automatic Verification of Effectful Programs.
Research Internship funded by MSR-Inria Joint Centre, 2018-09 to 2018-12:
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
Research Internship funded by MSR-Inria Joint Centre, 2016-01 to 2016-06:
Dijkstra Monads for Free
Exequiel Rivas
Starting Researcher Position at
Inria Paris
since 2019-03:
The Formal Semantics and Evolution of the F* Verification System
Roberto Blanco
Postdoctoral Researcher at
Inria Paris
since 2018-01:
Formally Secure Compilation Despite Dynamic Compromise
Adrien Durier
(Postdoctoral Researcher)
Antoine Van Muylder
Research Intern at
Inria Paris
starting 2019-05:
Relational Dijkstra Monads
[MSc student at
Paris 7
and
LMFI
]
Théo Laurent
Research Engineer at
Inria Paris
, since 2018-07:
Engineering and research work on F*
Research Intern at
Inria Paris
, 2017-03 to 2017-08:
Micro-policies backend for secure compilation
[MSc Student at
ENS Paris
and
MPRI
]
Ramkumar Ramachandra
(Research Intern / Engineer)
Past Group Members
Éric Tanter
(Visiting Professor, University of Chile)
Kenji Maillard
Graduated PhD student
at
Inria Paris
and
ENS Paris
from 2017-01 to 2019-11:
Principles of Program Verification for Arbitrary Monadic Effects
Cezar-Constantin Andrici
(Research Intern / Engineer, University of Iasi, Romania)
Florian Groult
Research Engineer at
Inria Paris
from 2018-11 to 2019-10:
Towards Formally Secure Compartmentalization for C
Research Intern at
Inria Paris
from 2018-04 to 2018-10:
Memory Sharing for a Compartmentalizing Compiler
[MSc student at
Orléans University
]
Elizabeth Labrada
Research Intern from 2018-10 to 2019-01:
Secure Compilation of Low* and C to WebAssembly.
[PhD Student at University of Chile]
Victor Dumitrescu
Research Engineer at
MSR-Inria
from 2017-01 to 2018-11:
Implementing Meta-programming and Tactics in F*
[Now Developer at
Nomadic Labs
working on
Tezos
]
Danel Ahman
Postdoctoral Researcher at
Inria Paris
from 2017-04 to 2018-09:
Semantic Foundations for F*
[Now PostDoc at
University of Ljubljana
]
Arthur Azevedo de Amorim
Graduated PhD student
at University of Pennsylvania; 2011-08 to 2017-10,
Co-Supervised with Benjamin C. Pierce:
A Methodology for Micro-Policies
Research Internship at Inria, 2014-03 to 2014-08:
Micro-Policies: Formally Verified, Tag-Based Security Monitors
[Now PostDoc at
Carnegie Mellon University
]
Amal Ahmed
(Visiting Professor, Northeastern University)
Aaron Weiss
(Visiting Researcher, Northeastern University)
Marco Stronati
PostDoctoral Researcher at
Inria Paris
, 2017-01 to 2017-12:
Formally Secure Compilation
[Now Developer at
Nomadic Labs
working on
Tezos
]
Guglielmo Fachini
Research Engineer at
Inria Paris
, 2017-01 to 2017-12:
Secure compilation proofs in Coq
[Now Developer at
Nozomi Networks
]
Ana Nora Evans
Visiting Researcher at
Inria Paris
, 2017-05 to 2017-08:
Software-fault isolation backend for secure compilation
[PhD Student at
University of Virginia
]
Clément Pit-Claudel
Research Intern at
Inria Paris
, 2017-07 to 2017-10:
Interactive proving and effect masking in F*
[PhD Student at
MIT
]
Tomer Libal
Research Engineer at
MSR-Inria
, 2017-01 to 2017-07: Refactoring the F* type-checker
[Now Assistant Professor at
The American University of Paris
]
William J. Bowman
Research Intern at
Inria Paris
, 2017-10 to 2017-12:
From Coq to Dependently Typed Assembly
[PhD Student at
Northeastern University
]
Yannis Juglaret
PhD Student funded by DGA/Inria grant, 2015-10 to 2016-09:
Micro-Policies: High-Assurance Hardware-Assisted Security Monitors
Research Internship at Inria, 2015-03 to 2015-08:
Towards a Fully Abstract Compiler Using Micro-Policies -- Secure Compilation for Mutually Distrustful Components
[Student at
Paris 7
and
MPRI
] [Now Engineer at
DGA-MI
]
Diane Gallois-Wong
Research Internship at Inria, 2016-03 to 2016-08:
Formalising Luck: Improved Probabilistic Semantics for Property-Based Generators
[MSc Student at
ENS Paris
and
MPRI
] [Intern at
TrustInSoft
] [Now PhD student at
LRI, Université Paris-Sud
]
Alejandro Aguirre
Research Internship at Inria, 2016-04 to 2016-08:
Towards a Provably Correct Encoding from F* to SMT
[MSc Student at
Paris 7
and
MPRI
] [Now PhD Student at
IMDEA Software Institute
]
Li-yao Xia
Research Internship at Inria, 2015-04 to 2015-08:
Integrating Functional Logic Programming with Constraint Solving for Random Generation of Structured Data
[MSc Student at
ENS Paris
and
MPRI
] [Now PhD student at
University of Pennsylvania
]
Simon Forest
Research Internship at Inria, 2015-03 to 2015-08:
Micro-F* in F*
[MSc Student at
ENS Paris
and
MPRI
] [MSc student at
LMFI
] [Now PhD Student at
École Polytechnique
]
Zoe Paraskevopoulou
Research Internship at Inria, 2014-04 to 2014-09:
QuickChick: A Coq Framework For Verified Property-Based Testing
(
thesis
)
[MSc Student at
NTU Athens
] [Then
MPRI
student] [Now PhD student at
Princeton University
]
Nick Giannarakis
Research Internship at Inria, 2014-04 to 2014-09:
Formally Verified Tag-Based Enforcement of Control Flow Integrity
(
thesis
)
[MSc Student at
NTU Athens
] [Then
MPRI
student] [Now PhD student at
Princeton University
]
Alex Busenius
Master's Thesis, Finished 2011-04-04:
Mechanized Formalization of a Transformation from an Extensible Spi Calculus to Java
Bachelor's Thesis, Finished 2008-10-28:
Expi2Java - An Extensible Code Generator for Security Protocols
[Student at
Saarland University
] [First employment
Capgemini
] [Now at
Luxoft
]
Thorsten Tarrach
Master's Thesis, Finished 2010-08-31:
Automatically Verifying "M" Modeling Language Constraints
(
thesis
)
Bachelor's Thesis, Finished 2008-10-27:
Spi2F# - A Prototype Code Generator for Security Protocols
[Student at
Saarland University
] [Then PhD student at
IST Austria
]
[Now research engineer at the
Austrian Institute of Technology (AIT)
]
Martin Grochulla
Master's Thesis, Finished 2009-01-06 (co-advised with Matteo Maffei)
Security Despite System Compromise with Zero-Knowledge Proofs
[Student at
Saarland University
] [
Then PhD student at the MPI-INF
] [Now at
IT Inkubator GmbH
]