Tahina Ramananandro

According to our database, Tahina Ramananandro authored at least 25 papers between 2008 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2023

ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER.

Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Nikhil Swamy

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

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

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

2022

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

Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

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

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, Min Xu

Proceedings of the SIGMOD '21: International Conference on Management of Data, 2021

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

IACR Cryptol. ePrint Arch., 2020

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, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella Béguelin

Proceedings of the 2020 IEEE Symposium on Security and Privacy, 2020

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, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella Béguelin

IACR Cryptol. ePrint Arch., 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

Proceedings of the 28th USENIX Security Symposium, 2019

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, Nikhil Swamy

Proceedings of the Programming Languages and Systems, 2019

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, Nikhil Swamy

CoRR, 2018

Certified concurrent abstraction layers.

Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, Tahina Ramananandro

Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

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

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017

Verified low-level programming embedded in F.

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

Proc. ACM Program. Lang., 2017

Verified Low-Level Programming Embedded in F^*.

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

CoRR, 2017

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, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella Béguelin, Jean Karim Zinzindohoue

Proceedings of the 2nd Summit on Advances in Programming Languages, 2017

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

Proceedings of the 2016 IEEE High Performance Extreme Computing Conference, 2016

A unified Coq framework for verifying C programs with floating-point computations.

Tahina Ramananandro, Paul Mountcastle, Benoît Meister, Richard Lethin

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

2015

Deep Specifications and Certified Abstraction Layers.

Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, Yu Guo

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

A Compositional Semantics for Verified Separate Compilation and Linking.

Tahina Ramananandro, Zhong Shao, Shu-Chun Weng, Jérémie Koenig, Yuchen Fu

Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

2014

End-to-end verification of stack-space bounds for C programs.

Quentin Carbonneaux, Jan Hoffmann, Tahina Ramananandro, Zhong Shao

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014

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

PhD thesis, 2012

A mechanized semantics for C++ object construction and destruction, with applications to resource management.

Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy

Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

2011

Formal verification of object layout for c++ multiple inheritance.

Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

2008

<i>Mondex</i> , an electronic purse: specification and refinement checks with the <i>Alloy</i> model-finding method.

Tahina Ramananandro

Formal Aspects Comput., 2008