Tahina Ramananandro

According to our database1, Tahina Ramananandro authored at least 20 papers between 2008 and 2020.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

On csauthors.net:

Bibliography

2020
A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer.
IACR Cryptol. ePrint Arch., 2020


2019
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider.
IACR Cryptol. ePrint Arch., 2019

EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats.
Proceedings of the 28th USENIX Security Symposium, 2019

Meta-F ^\star : Proof Automation with SMT, Tactics, and Metaprograms.
Proceedings of the Programming Languages and Systems, 2019

2018
Meta-F*: Metaprogramming and Tactics in an Effectful Program Verifier.
CoRR, 2018

Certified concurrent abstraction layers.
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.
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017
Verified low-level programming embedded in F.
Proc. ACM Program. Lang., 2017

Verified Low-Level Programming Embedded in F<sup>*</sup>.
CoRR, 2017


2016
Accelerated low-rank updates to tensor decompositions.
Proceedings of the 2016 IEEE High Performance Extreme Computing Conference, 2016

A unified Coq framework for verifying C programs with floating-point computations.
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

2015
Deep Specifications and Certified Abstraction Layers.
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

A Compositional Semantics for Verified Separate Compilation and Linking.
Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

2014
End-to-end verification of stack-space bounds for C programs.
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).
PhD thesis, 2012

A mechanized semantics for C++ object construction and destruction, with applications to resource management.
Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

2011
Formal verification of object layout for c++ multiple inheritance.
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.
Formal Aspects Comput., 2008


  Loading...