Mondex , an electronic purse: specification and refinement checks with the Alloy model-finding method. - Tahina Ramananandro (Formal Aspects Comput., 2008)

Formal verification of object layout for c++ multiple inheritance. - Tahina Ramananandro; Gabriel Dos Reis; Xavier Leroy (POPL, 2011)

A mechanized semantics for C++ object construction and destruction, with applications to resource management. - Tahina Ramananandro; Gabriel Dos Reis; Xavier Leroy (POPL, 2012)

Mechanized Formal Semantics and Verified Compilation for C++ Objects. (Les objets en C++ : sémantique formelle mécanisée et compilation vérifiée). - Tahina Ramananandro (2012)

End-to-end verification of stack-space bounds for C programs. - Quentin Carbonneaux; Jan Hoffmann 002; Tahina Ramananandro; Zhong Shao 001 (PLDI, 2014)

A Compositional Semantics for Verified Separate Compilation and Linking. - Tahina Ramananandro; Zhong Shao 001; Shu-Chun Weng; Jérémie Koenig; Yuchen Fu (CPP, 2015)

Deep Specifications and Certified Abstraction Layers. - Ronghui Gu; Jérémie Koenig; Tahina Ramananandro; Zhong Shao 001; Xiongnan (Newman) Wu; Shu-Chun Weng; Haozhong Zhang; Yu Guo (POPL, 2015)

A unified Coq framework for verifying C programs with floating-point computations. - Tahina Ramananandro; Paul Mountcastle; Benoît Meister; Richard Lethin (CPP, 2016)

Accelerated low-rank updates to tensor decompositions. - Muthu Manikandan Baskaran; Matthew Harper Langston; Tahina Ramananandro; David Bruns-Smith; Tom Henretty; James R. Ezick; Richard Lethin (HPEC, 2016)

Everest: Towards a Verified, Drop-in Replacement of HTTPS. - Karthikeyan Bhargavan; Barry Bond; Antoine Delignat-Lavaud; Cédric Fournet; Chris Hawblitzel; Catalin Hritcu; Samin Ishtiaq; Markulf Kohlweiss; K. Rustan M. Leino; Jay R. Lorch; Kenji Maillard; Jianyang Pan; et al. (SNAPL, 2017)

Verified Low-Level Programming Embedded in F*. - Jonathan Protzenko; Jean Karim Zinzindohoué; Aseem Rastogi; Tahina Ramananandro; Peng Wang 048; Santiago Zanella-Béguelin; Antoine Delignat-Lavaud; Catalin Hritcu; Karthikeyan Bhargavan; Cédric Fournet; Nikhil Swamy (CoRR, 2017)

Verified low-level programming embedded in F. - Jonathan Protzenko; Jean Karim Zinzindohoué; Aseem Rastogi; Tahina Ramananandro; Peng Wang 048; Santiago Zanella-Béguelin; Antoine Delignat-Lavaud; Catalin Hritcu; Karthikeyan Bhargavan; Cédric Fournet; Nikhil Swamy (Proc. ACM Program. Lang., 2017)

A monadic framework for relational verification: applied to information security, program equivalence, and optimizations. - Niklas Grimm; Kenji Maillard; Cédric Fournet; Catalin Hritcu; Matteo Maffei; Jonathan Protzenko; Tahina Ramananandro; Aseem Rastogi; Nikhil Swamy; Santiago Zanella-Béguelin (CPP, 2018)

Certified concurrent abstraction layers. - Ronghui Gu; Zhong Shao 001; Jieung Kim; Xiongnan (Newman) Wu; Jérémie Koenig; Vilhelm Sjöberg; Hao Chen 023; David Costanzo; Tahina Ramananandro (PLDI, 2018)

Meta-F*: Metaprogramming and Tactics in an Effectful Program Verifier. - 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; et al. (CoRR, 2018)

Meta-F ^ star : Proof Automation with SMT, Tactics, and Metaprograms. - 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; et al. (ESOP, 2019)

EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. - Tahina Ramananandro; Antoine Delignat-Lavaud; Cédric Fournet; Nikhil Swamy; Tej Chajed; Nadim Kobeissi; Jonathan Protzenko (USENIX Security Symposium, 2019)

EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. - Jonathan Protzenko; Bryan Parno; Aymeric Fromherz; Chris Hawblitzel; Marina Polubelova; Karthikeyan Bhargavan; Benjamin Beurdouche; Joonwon Choi; Antoine Delignat-Lavaud; Cédric Fournet; Tahina Ramananandro; Aseem Rastogi; et al. (IACR Cryptol. ePrint Arch., 2019)

EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. - 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; et al. (SP, 2020)

A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer. - Antoine Delignat-Lavaud; Cédric Fournet; Bryan Parno; Jonathan Protzenko; Tahina Ramananandro; Jay Bosamiya; Joseph Lallemand; Itsaka Rakotonirina; Yi Zhou 025 (IACR Cryptol. ePrint Arch., 2020)

FastVer: Making Data Integrity a Commodity. - Arvind Arasu; Badrish Chandramouli; Johannes Gehrke; Esha Ghosh; Donald Kossmann; Jonathan Protzenko; Ravi Ramamurthy; Tahina Ramananandro; Aseem Rastogi; Srinath T. V. Setty; Nikhil Swamy; Alexander van Renen; et al. (SIGMOD Conference, 2021)

Steel: proof-oriented programming in a dependently typed concurrent separation logic. - Aymeric Fromherz; Aseem Rastogi; Nikhil Swamy; Sydney Gibson; Guido Martínez; Denis Merigoux; Tahina Ramananandro (Proc. ACM Program. Lang., 2021)

Hardening attack surfaces with formally proven binary format parsers. - Nikhil Swamy; Tahina Ramananandro; Aseem Rastogi; Irina Spiridonova; Haobin Ni; Dmitry Malloy; Juan Vazquez; Michael Tang; Omar Cardona; Arti Gupta (PLDI, 2022)

FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores. - Arvind Arasu; Tahina Ramananandro; Aseem Rastogi; Nikhil Swamy; Aymeric Fromherz; Kesha Hietala; Bryan Parno; Ravi Ramamurthy (CPP, 2023)

ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER. - Haobin Ni; Antoine Delignat-Lavaud; Cédric Fournet; Tahina Ramananandro; Nikhil Swamy (CPP, 2023)

DiffSpec: Differential Testing with LLMs using Natural Language Specifications and Code Artifacts. - Nikitha Rao; Elizabeth Gilbert; Tahina Ramananandro; Nikhil Swamy; Claire Le Goues; Sarah Fakhoury (CoRR, 2024)

3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers. - Sarah Fakhoury; Markus Kuppe 001; Shuvendu K. Lahiri; Tahina Ramananandro; Nikhil Swamy (ICSE, 2025)

PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs. - Gabriel Ebner; Guido Martínez; Aseem Rastogi; Thibault Dardinier; Megan Frisella; Tahina Ramananandro; Nikhil Swamy (Proc. ACM Program. Lang., 2025)

Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE. - Tahina Ramananandro; Gabriel Ebner; Guido Martínez; Nikhil Swamy (CoRR, 2025)