Tahina Ramananandro

31 papers A* 11A 1B 5Journal 10Unranked 3
YearRankTypeTitle / Venue / Authors
2025 A* conf
3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers.
ICSE
Sarah Fakhoury, Markus Kuppe, Shuvendu K. Lahiri, Tahina Ramananandro, Nikhil Swamy
2025 J jnl
PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs.
Proc. ACM Program. Lang.
Gabriel Ebner, Guido Martínez, Aseem Rastogi, Thibault Dardinier, Megan Frisella, Tahina Ramananandro, Nikhil Swamy
2025 A* conf
Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE.
CCS
Tahina Ramananandro, Gabriel Ebner, Guido Martínez, Nikhil Swamy
2025 J jnl
Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE.
CoRR
Tahina Ramananandro, Gabriel Ebner, Guido Martínez, Nikhil Swamy
2024 J jnl
3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers.
CoRR
Sarah Fakhoury, Markus Kuppe, Shuvendu K. Lahiri, Tahina Ramananandro, Nikhil Swamy
2024 J jnl
DiffSpec: Differential Testing with LLMs using Natural Language Specifications and Code Artifacts.
CoRR
Nikitha Rao, Elizabeth Gilbert, Tahina Ramananandro, Nikhil Swamy, Claire Le Goues, Sarah Fakhoury
2023 B conf
ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER.
CPP
Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Nikhil Swamy
2023 B conf
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores.
CPP
Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, Ravi Ramamurthy
2022 A* conf
Hardening attack surfaces with formally proven binary format parsers.
PLDI
Nikhil Swamy, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael Tang, Omar Cardona, Arti Gupta
2021 A* conf
A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer.
SP
Antoine Delignat-Lavaud, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, Yi Zhou
2021 — conf
FastVer: Making Data Integrity a Commodity.
SIGMOD Conference
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, Min Xu
2021 J jnl
Steel: proof-oriented programming in a dependently typed concurrent separation logic.
Proc. ACM Program. Lang.
Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido Martínez, Denis Merigoux, Tahina Ramananandro
2020 J jnl
A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer.
IACR Cryptol. ePrint Arch.
Antoine Delignat-Lavaud, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, Yi Zhou
2020 A* conf
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider.
SP
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 M. Wintersteiger, Santiago Zanella-Béguelin
2019 J jnl
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider.
IACR Cryptol. ePrint Arch.
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, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
2019 A* conf
EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats.
USENIX Security Symposium
Tahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, Jonathan Protzenko
2019 A conf
Meta-F ^\star : Proof Automation with SMT, Tactics, and Metaprograms.
ESOP
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
2018 B conf
A monadic framework for relational verification: applied to information security, program equivalence, and optimizations.
CPP
Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin
2018 A* conf
Certified concurrent abstraction layers.
PLDI
Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, Tahina Ramananandro
2018 J jnl
Meta-F*: Metaprogramming and Tactics in an Effectful Program Verifier.
CoRR
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
2017 — conf
Everest: Towards a Verified, Drop-in Replacement of HTTPS.
SNAPL
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, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean Karim Zinzindohoue
2017 J jnl
Verified Low-Level Programming Embedded in F
CoRR
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
2017 J jnl
Verified low-level programming embedded in F.
Proc. ACM Program. Lang.
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
2016 B conf
A unified Coq framework for verifying C programs with floating-point computations.
CPP
Tahina Ramananandro, Paul Mountcastle, Benoît Meister, Richard Lethin
2016 — conf
Accelerated low-rank updates to tensor decompositions.
HPEC
Muthu Manikandan Baskaran, Matthew Harper Langston, Tahina Ramananandro, David Bruns-Smith, Tom Henretty, James R. Ezick, Richard Lethin
2015 B conf
A Compositional Semantics for Verified Separate Compilation and Linking.
CPP
Tahina Ramananandro, Zhong Shao, Shu-Chun Weng, Jérémie Koenig, Yuchen Fu
2015 A* conf
Deep Specifications and Certified Abstraction Layers.
POPL
Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, Yu Guo
2014 A* conf
End-to-end verification of stack-space bounds for C programs.
PLDI
Quentin Carbonneaux, Jan Hoffmann, Tahina Ramananandro, Zhong Shao
2012 A* conf
A mechanized semantics for C++ object construction and destruction, with applications to resource management.
POPL
Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy
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
2011 A* conf
Formal verification of object layout for c++ multiple inheritance.
POPL
Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy