Tahina Ramananandro
Tahina Ramananandro
Microsoft Research
Verified email at ramananandro.org - Homepage
Title
Cited by
Cited by
Year
Deep specifications and certified abstraction layers
R Gu, J Koenig, T Ramananandro, Z Shao, X Wu, SC Weng, H Zhang, ...
ACM SIGPLAN Notices 50 (1), 595-608, 2015
1742015
Verified low-level programming embedded in F.
J Protzenko, JK Zinzindohoué, A Rastogi, T Ramananandro, P Wang, ...
Proc. ACM program. lang. 1 (ICFP), 17:1-17:29, 2017
882017
End-to-end verification of stack-space bounds for C programs
Q Carbonneaux, J Hoffmann, T Ramananandro, Z Shao
Proceedings of the 35th ACM SIGPLAN Conference on Programming Language …, 2014
662014
Everest: Towards a verified, drop-in replacement of HTTPS
K Bhargavan, B Bond, A Delignat-Lavaud, C Fournet, C Hawblitzel, ...
2nd Summit on Advances in Programming Languages (SNAPL 2017), 2017
622017
Mondex, an electronic purse: specification and refinement checks with the Alloy model-finding method
T Ramananandro
Formal Aspects of Computing 20 (1), 21-39, 2008
512008
Evercrypt: A fast, verified, cross-platform cryptographic provider
J Protzenko, B Parno, A Fromherz, C Hawblitzel, M Polubelova, ...
2020 IEEE Symposium on Security and Privacy (SP), 983-1002, 2020
372020
Certified concurrent abstraction layers
R Gu, Z Shao, J Kim, X Wu, J Koenig, V Sjöberg, H Chen, D Costanzo, ...
ACM SIGPLAN Notices 53 (4), 646-661, 2018
302018
Formal verification of object layout for C++ multiple inheritance
T Ramananandro, G Dos Reis, X Leroy
ACM SIGPLAN Notices 46 (1), 67-80, 2011
262011
A unified Coq framework for verifying C programs with floating-point computations
T Ramananandro, P Mountcastle, B Meister, R Lethin
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and …, 2016
242016
Meta-F: Proof Automation with SMT, Tactics, and Metaprograms
G Martínez, D Ahman, V Dumitrescu, N Giannarakis, C Hawblitzel, ...
European Symposium on Programming, 30-59, 2019
202019
Everparse: Verified secure zero-copy parsers for authenticated message formats
T Ramananandro, A Delignat-Lavaud, C Fournet, N Swamy, T Chajed, ...
28th {USENIX} Security Symposium ({USENIX} Security 19), 1465-1482, 2019
202019
A compositional semantics for verified separate compilation and linking
T Ramananandro, Z Shao, SC Weng, J Koenig, Y Fu
Proceedings of the 2015 Conference on Certified Programs and Proofs, 3-14, 2015
192015
A mechanized semantics for C++ object construction and destruction, with applications to resource management
T Ramananandro, G Dos Reis, X Leroy
ACM SIGPLAN Notices 47 (1), 521-532, 2012
152012
A monadic framework for relational verification: applied to information security, program equivalence, and optimizations
N Grimm, K Maillard, C Fournet, C Hriţcu, M Maffei, J Protzenko, ...
Proceedings of the 7th ACM SIGPLAN International Conference on Certified …, 2018
142018
Verified low-level programming embedded in F*. PACMPL 1, ICFP (2017), 17: 1–17: 29
J Protzenko, JK Zinzindohoué, A Rastogi, T Ramananandro, P Wang, ...
102017
Verified low-level programming embedded in F*
K Bhargavan, A Delignat-Lavaud, C Fournet, C Hritcu, J Protzenko, ...
arXiv preprint arXiv:1703.00053, 2017
92017
A security model and fully verified implementation for the IETF QUIC record layer
A Delignat-Lavaud, C Fournet, B Parno, J Protzenko, T Ramananandro, ...
2021 IEEE Symposium on Security and Privacy (SP), 1162-1178, 2021
82021
Verified Low-Level Programming Embedded in F*. PACMPL 1, ICFP (Sept. 2017), 17: 1ś17: 29
J Protzenko, JK Zinzindohoué, A Rastogi, T Ramananandro, P Wang, ...
82017
Accelerated low-rank updates to tensor decompositions
M Baskaran, MH Langston, T Ramananandro, D Bruns-Smith, T Henretty, ...
2016 IEEE High Performance Extreme Computing Conference (HPEC), 1-7, 2016
72016
Systems and methods for energy proportional scheduling
MM Baskaran, T Henretty, A Johnson, A Konstantinidis, MH Langston, ...
US Patent 10,540,107, 2020
32020
The system can't perform the operation now. Try again later.
Articles 1–20