Short Bio

I am a Principal Applied Scientist at Amazon with the S3 Automated Reasoning Group. From 2018 to 2022 I was a researcher at Arm. Before that, from 2015 to 2018 I was 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. From 2012 to 2015 I served as Visiting Assistant Professor at Purdue University in the C.S. department where I worked 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. in 2010 under the supervision of Gérard Boudol at the INDES team at INRIA Sophia Antipolis, France. During 2006 and 2007 I worked under the supervision of Marieke Huisman at the Everest team. I obtained my degree on C.S. at Famaf, University of Córdoba, Argentina in 2005.

Research Interests

My current research interests are distributed systems security and consistency. Hardware and software relaxed memory models, the 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, distributed systems, and security.

Publications

• Transactuations: Where Transactions Meet the Physical World. With T. Leesatapornwongsa, A. Sengupta, M. Saeida Ardekani, and C. A. Stuardo. In ACM Transactions on Computer Systems.
• PLASMA: Programmable Elasticity for Stateful Cloud Computing Applications. With B. Sang, P-L. Roman, P. Eugster. H. Lu, and S. Ravi. In EuroSys'20.
• Proving the safety of highly-available distributed objects. With S. Nair, and M. Shapiro. In ESOP'20.
• Replication-Aware Linearizability. With C. Wang, C. Enea, and S. Orhun Mutluergil. In PLDI'19. [Video]
• Invariant Safety for Distributed Applications. With S. Nair, and M. Shapiro. In PaPoC@EuroSys 2019.
• Ensuring referential integrity under causal consistency. With M. Shapiro, A. Bieniusa, and Peter Zeller. In PaPoC@EuroSys 2018.
• Programmable Elasticity for Actor-based Cloud Applications. With B. Sang, S. Ravi, Najafzadeh M. , M. Saeida Ardekani, P. Eugster. In PLOS'17.
• A Programmable Buffer Management Platform. With K. Kogan, D. Menikkumbura, Y. Noh, S. Nikolenko, A. Sirotkin, and P. Eugster. To appear in ICNP'17.
• Verifying a Concurrent Garbage Collector using a Rely-Guarantee Methodology. With Y. Zakowski, D. Cachera, D. Demange, D. Pichardie, S. Jagannathan, and J. Vitek. In ITP'17.
  • The formalization.
• Composing Middlebox and Traffic Engineering Policies in SDNs. With Y. Chang, S. Rao, and T. Rompf at INFOCOM Workshop SWFAN'17.
• Programming Scalable Cloud Services with AEON. With B. Sang, M. Saeida Ardekani, S. Ravi, and P. Eugster at Middleware'16.
  • Project Page.
• Consistency in 3D [TR]. With M. Shapiro and M. Saeida Ardekani. Invited contribution at CONCUR'16.
• Automatically Learning Shape Specifications. With He Zhu and S. Jagannathan at PLDI'16.
  • Project Page.
• BASEL (Buffer mAnagement SpEcification Language). With K. Kogan, D. Menikkumbura, T. Noh, S. Nikolenko, and P. Eugster at ANCS'16.
• Poling: SMT Aided Linearizability Proofs. With He Zhu and S. Jagannathan at CAV'15.
  • Project Page.
• Cooking the Books: Formalizing JMM Implementation Recipes. With J. Vitek and S. Jagannathan at ECOOP'15. [Video]
  • Extended Version with proofs.
• Atomicity Refinement for Verified Compilation. With S. Jagannathan, V. Laporte, D. Pichardie and J. Vitek. Appeared at TOPLAS'14. Presented at PLDI'14.
  • The formalization.
• Studying Operational Models of Relaxed Concurrency Concurrency at TGC'13.
• Quarantining Weakness: Compositional Reasoning Under Relaxed Memory Models. With R. Jagadeesan, J. Riely and C. Pitcher at ESOP'13.
• Relaxed Semantics of Concurrent Programming Languages (long version). With Gérard Boudol and Bernard Serpette at Express/SOS'12.
  • The associated simulator.
• Brookes is Relaxed, Almost! With Radha Jagadeesan and James Riely at FoSSaCS'12.
• Operational Semantics for Relaxed Memory Models (Thesis) 2010.
• A Theory of Speculative Computation. With Gérard Boudol at ESOP'10.
• Relaxed memory models: an operational approach. With Gérard Boudol at POPL'09.
• BicolanoMT: a formalization of multi-threaded Java at bytecode level. With Marieke Huisman at Bytecode'08.
  • The formalization.
• The Java memory model: a formal explanation. With Marieke Huisman in Verification and Analysis of Multi-threaded Java-like Programs (VAMP'07).
  • The formalization.