Some Research Projects
Publications
In the News
International peer-reviewed conferences and workshops
-
Tahina Ramananandro,
Gabriel Ebner,
Guido Martínez,
Nikhil
Swamy
Secure Parsing and Serializing with Separation Logic Applied
to CBOR, CDDL and COSE
CCS 2025
Distinguished
Artifact Award
-
Gabriel Ebner,
Guido
Martínez,
Aseem
Rastogi,
Thibault Dardinier,
Megan Frisella,
Tahina Ramananandro,
Nikhil
Swamy
PulseCore: An Impredicative Concurrent
Separation Logic for Dependently Typed Programs
PLDI 2025
-
Sarah
Fakhoury,
Markus Kuppe,
Shuvendu Lahiri,
Tahina Ramananandro,
Nikhil Swamy
3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers
ICSE 2025
-
Arvind Arasu,
Tahina Ramananandro,
Aseem
Rastogi,
Nikhil
Swamy,
Aymeric Fromherz,
Kesha Hietala,
Bryan Parno,
Ravi
Ramamurthy
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value
Stores
CPP 2023
-
Haobin Ni,
Antoine Delignat-Lavaud,
Cédric
Fournet,
Tahina Ramananandro,
Nikhil
Swamy
ASN1*: Provably Correct Non-Malleable Parsing for ASN.1 DER
CPP 2023
-
Nikhil
Swamy,
Tahina Ramananandro,
Aseem
Rastogi,
Irina
Spiridonova,
Haobin Ni ,
Dmitry Malloy,
Juan Vazquez,
Michael Tang,
Omar Cardona,
Arti Gupta
Hardening Attack Surfaces with Formally Proven
Binary Format Parsers
PLDI 2022
-
Aymeric Fromherz,
Aseem
Rastogi,
Nikhil
Swamy,
Sydney Gibson,
Guido
Martínez,
Denis Merigoux,
Tahina Ramananandro
Steel: Proof-oriented Programming in a Dependently Typed
Concurrent Separation Logic
ICFP
2021
-
Arvind Arasu,
Johannes
Gehrke,
Esha
Ghosh,
Donald
Kossmann,
Jonathan Protzenko,
Ravi
Ramamurthy,
Tahina Ramananandro,
Aseem
Rastogi,
Srinath Setty,
Nikhil
Swamy,
Alexander van Renen,
Min Xu
FastVer: Making Data Integrity a Commodity
ACM SIGMOD 2021
-
Antoine Delignat-Lavaud,
Cédric
Fournet,
Bryan Parno,
Jonathan Protzenko,
Tahina Ramananandro,
Jay Bosamiya,
Joseph Lallemand,
Itsaka Rakotonirina,
Yi Zhou
A Security Model and Fully Verified Implementation for the
IETF QUIC Record Layer
IEEE S&P
2021 ("Oakland")
-
Jonathan Protzenko,
Bryan Parno,
Aymeric Fromherz,
Chris
Hawblitzel,
Marina Polubelova,
Karthikeyan Bhargavan,
Benjamin Beurdouche,
Joonwon Choi,
Antoine Delignat-Lavaud,
Cédric
Fournet,
Natalia Kulatova,
Tahina Ramananandro,
Aseem
Rastogi,
Nikhil
Swamy,
Christoph
Wintersteiger,
Santiago
Zanella-Béguelin
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider
IEEE S&P
2020 ("Oakland")
-
Tahina Ramananandro,
Antoine Delignat-Lavaud,
Cédric
Fournet,
Nikhil
Swamy,
Tej Chajed,
Nadim Kobeissi,
Jonathan Protzenko
EverParse: Verified Secure Zero-Copy Parsers for
Authenticated Message Formats
USENIX Security 2019
-
Guido
Martínez,
Danel Ahman,
Victor Dumitrescu,
Nick Giannarakis,
Chris
Hawblitzel,
Catalin
Hritcu,
Monal Narasimhamurthy,
Zoe Paraskevopoulou,
Clément Pit-Claudel,
Jonathan Protzenko,
Tahina Ramananandro,
Aseem
Rastogi,
Nikhil
Swamy
Meta-F*: Proof Automation with SMT,
Tactics and Metaprograms
ESOP
2019
-
Ronghui Gu,
Zhong Shao,
Jieung Kim,
Xiongnan (Newman) Wu,
Jérémie
Koenig,
Vilhelm Sjöberg,
Hao Chen,
David Costanzo,
Tahina Ramananandro
Certified Concurrent Abstraction Layers
PLDI 2018
-
Niklas Grimm,
Kenji Maillard,
Cédric
Fournet,
Catalin
Hritcu,
Matteo
Maffei,
Jonathan Protzenko,
Tahina Ramananandro,
Aseem
Rastogi,
Nikhil
Swamy,
Santiago
Zanella-Béguelin
A Monadic Approach to Relational Verification:
Applied to Information Security, Program Equivalence, and
Optimizations
CPP 2018
-
Jonathan Protzenko,
Jean-Karim Zinzindohoué,
Aseem
Rastogi,
Tahina Ramananandro,
Peng Wang,
Santiago Zanella-Béguelin,
Antoine Delignat-Lavaud,
Catalin Hritcu,
Karthikeyan Bhargavan,
Cédric Fournet,
Nikhil Swamy
Verified Low-Level Programming Embedded in F*
ICFP 2017
-
Karthikeyan Bhargavan,
Barry Bond,
Antoine Delignat-Lavaud,
Cédric Fournet,
Chris
Hawblitzel,
Catalin Hritcu,
Samin Ishtiaq,
Markulf Kohlweiss,
Rustan Leino,
Jay Lorch,
Kenji Maillard,
Jianyang Pang,
Bryan Parno,
Jonathan Protzenko,
Tahina Ramananandro,
Ashay Rane,
Aseem
Rastogi,
Nikhil Swamy,
Laure Thompson,
Peng Wang,
Santiago Zanella-Béguelin,
Jean-Karim Zinzindohoué
Everest: Towards a Verified, Drop-in Replacement of HTTPS
SNAPL 2017
-
Muthu Baskaran, M. Harper Langston, Tahina Ramananandro, David
Bruns-Smith, Tom Henretty, James Ezick, Richard Lethin
Accelerated Low-Rank Updates to Tensor Decompositions
HPEC 2016
- Tahina Ramananandro, Paul Mountcastle, Benoît Meister, Richard
Lethin
A Unified Coq Framework for Verifying C Programs with Floating-Point
Computations
CPP 2016
- Tahina Ramananandro,
Zhong Shao,
Shu-Chun Weng,
Jérémie Koenig and
Yuchen Fu
A Compositional Semantics for Verified Separate Compilation and
Linking
CPP 2015
-
Ronghui
Gu,
Jérémie Koenig,
Tahina Ramananandro,
Zhong Shao,
Shu-Chun Weng,
Xiongnan (Newman) Wu,
Haozhong
Zhang and
Yu Guo
Deep specifications and Certified Abstraction Layers
POPL 2015
- Quentin Carbonneaux,
Jan Hoffmann, Tahina Ramananandro
, Zhong Shao
End-to-End Verification of Stack-Space Bounds
for C Programs
PLDI 2014
- Tahina Ramananandro, Gabriel Dos
Reis, Xavier
Leroy
A Mechanized Semantics for C++ Object
Construction and Destruction, with Applications to Resource
Management
POPL 2012
- Tahina Ramananandro, Gabriel Dos
Reis, Xavier
Leroy
Formal verification of
object layout for C++ multiple inheritance
POPL 2011
International peer-reviewed journals
Theses
-
Mechanized Formal Semantics and Verified Compilation for C++
Objects
Ph. D. thesis, University Paris. Diderot (Paris 7)
Directed by Xavier Leroy,
Gallium, INRIA Paris-Rocquencourt
Successfully defended on January 10th, 2012 at École normale supérieure.
-
Vérification formelle d'une implémentation d'un
gestionnaire de mémoire pour un compilateur certifié
Master's thesis, École normale supérieure
Directed by Xavier Leroy,
Gallium, INRIA Paris-Rocquencourt
Successfully defended in September 2007 at École normale supérieure.
-
Vérification formelle d'algorithmes probabilistes
Bachelor's thesis, University Paris. Diderot (Paris 7)
Directed by Laurent Théry and Philippe
Audebaud,
Marelle, INRIA Sophia-Antipolis
Successfully defended in September 2005 at École normale supérieure.