I am an Assistant Professor at the Modeling and Verification team of the Institut de Recherche en Informatique Fondamentale (IRIF) lab at the Université Paris Diderot -- Paris 7. Before I was a Visiting Assistant Professor at Purdue University in the C.S. department where I enjoyed working with Suresh Jagannathan and Jan Vitek. During 2011 I was a postdoctoral fellow at DePaul University at Chicago working with Radha Jagadeesan, James Riely and Corin Pitcher. I obtained my Ph.D. under the supervision of Gérard Boudol in 2010 at the INDES team at INRIA Sophia Antipolis, France. During 2006 and 2007 I enjoyed working with Marieke Huisman at the Everest team. I obtained my degree on C.S. at Famaf, University of Córdoba, Argentina in 2005.
My current research topics are memory models, semantics of shared memory and distributed systems, verified compilers, and the verification of concurrent and distributed algorithms. I am broadly interested in verification and formal methods, concurrency, and distributed systems.
- Programming Scalable Cloud Services with AEON. With B. Sang, M. Saeida Ardekani, S. Ravi, and P. Eugster at Middleware'16.
- Automatically Learning Shape Specifications. With He Zhu and S. Jagannathan at PLDI'16.
- BASEL (Buffer mAnagement SpEcification Language). With K. Kogan, D. Menikkumbura, T. Noh, S. Nikolenko, and P. Eugster at ANCS'16.
- Cooking the Books: Formalizing JMM Implementation Recipes. With
J. Vitek and
Jagannathan at ECOOP'15.
- Extended Version with proofs.
- Atomicity Refinement
for Verified Compilation. With
D. Pichardie and
Appeared at TOPLAS'14. Presented at
- The formalization.
- Quarantining Weakness: Compositional Reasoning Under Relaxed Memory Models. With R. Jagadeesan, J. Riely and C. Pitcher at ESOP'13.
Semantics of Concurrent Programming Languages (long version). With
Gérard Boudol and
- The associated simulator.
- Operational Semantics for Relaxed Memory Models (Thesis) 2010.
- BicolanoMT: a
formalization of multi-threaded Java at bytecode
level. With Marieke
Huisman at Bytecode'08.
- The formalization.