Travelled to:1 × India
1 × United Kingdom
2 × USA
Collaborated with:G.D.Reis X.Leroy Z.Shao Q.Carbonneaux J.Hoffmann R.Gu J.Koenig X.(.Wu S.Weng H.Zhang Y.Guo Jieung Kim V.Sjöberg Hao Chen 0023 David Costanzo G.Martínez D.Ahman V.Dumitrescu N.Giannarakis C.Hawblitzel C.Hritcu M.Narasimhamurthy Z.Paraskevopoulou C.Pit-Claudel J.Protzenko A.Rastogi N.Swamy
Talks about:abstract (2) certifi (2) object (2) verif (2) layer (2) end (2) metaprogram (1) construct (1) destruct (1) resourc (1)
Person: Tahina Ramananandro
DBLP: Ramananandro:Tahina
Contributed to:
2015
201420122011
20192018Wrote 6 papers:
- POPL-2015-GuKRSWWZG #abstraction #specification
- Deep Specifications and Certified Abstraction Layers (RG, JK, TR, ZS, X(W, SCW, HZ, YG), pp. 595–608.
- PLDI-2014-Carbonneaux0RS #bound #c #source code #verification
- End-to-end verification of stack-space bounds for C programs (QC, JH, TR, ZS), p. 30.
- POPL-2012-RamananandroRL #c++ #resource management #semantics
- A mechanized semantics for C++ object construction and destruction, with applications to resource management (TR, GDR, XL), pp. 521–532.
- POPL-2011-RamananandroRL #c++ #inheritance #layout #multi #verification
- Formal verification of object layout for c++ multiple inheritance (TR, GDR, XL), pp. 67–80.
- ESOP-2019-MartinezADGHHNP #automation #metaprogramming #proving #smt
- Meta-F* : Proof Automation with SMT, Tactics, and Metaprograms (GM, DA, VD, NG, CH, CH, MN, ZP, CPC, JP, TR, AR, NS), pp. 30–59.
- PLDI-2018-GuSKWKS0CR #abstraction #concurrent
- Certified concurrent abstraction layers (RG, ZS, JK, X(W, JK, VS, HC0, DC, TR), pp. 646–661.