Gustavo Petri

Gustavo Petri

Principal Applied Scientist, Amazon — S3 Automated Reasoning

Formal methods · verification · concurrency · distributed systems

Short Bio

I am a Principal Applied Scientist at Amazon, where I lead a team bringing formal methods and automated reasoning to production at scale with the S3 Automated Reasoning Group. Previously I was a Principal Research Engineer at Arm (2018–2022), leading formal verification of the Arm Confidential Computing Architecture, and an Associate Professor (Maître de Conférences) in the Modeling and Verification team at IRIF, Université Paris Diderot (2015–2018). Earlier I was a Visiting Assistant Professor at Purdue University (2012–2015). I received my Ph.D. in 2010 from INRIA Sophia Antipolis, and my C.S. degree from FaMAF, University of Córdoba, Argentina, in 2005.

Research Interests

I work on formal verification, automated reasoning, programming languages, and the design and verification of concurrent and distributed systems — including relaxed memory models and confidential computing. I particularly enjoy applying theory to real systems and hardware.

Publications

  1. High Fidelity Models for Large Scale Stateful Services. With N. Jaber, D. Jin, B. Kragl, E. Magnago, T. Tarrach, and S. Tasiran. To appear at OSDI 2026.
  2. A Verification Methodology for the Arm® Confidential Computing Architecture: From a Secure Specification to Safe Implementations. With Anthony C. J. Fox, Gareth Stockwell, Shale Xiong, Hanno Becker, Dominic P. Mulligan, and Nathan Chong. In OOPSLA 2023.
  3. 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.
  4. PLASMA: Programmable Elasticity for Stateful Cloud Computing Applications. With B. Sang, P-L. Roman, P. Eugster, H. Lu, and S. Ravi. In EuroSys'20.
  5. Proving the Safety of Highly-Available Distributed Objects. With S. Nair, and M. Shapiro. In ESOP'20.
  6. Replication-Aware Linearizability. With C. Wang, C. Enea, and S. Orhun Mutluergil. In PLDI'19. [Video]
  7. Invariant Safety for Distributed Applications. With S. Nair, and M. Shapiro. In PaPoC@EuroSys 2019.
  8. Ensuring Referential Integrity under Causal Consistency. With M. Shapiro, A. Bieniusa, and Peter Zeller. In PaPoC@EuroSys 2018.
  9. Programmable Elasticity for Actor-based Cloud Applications. With B. Sang, S. Ravi, Najafzadeh M., M. Saeida Ardekani, P. Eugster. In PLOS'17.
  10. A Programmable Buffer Management Platform. With K. Kogan, D. Menikkumbura, Y. Noh, S. Nikolenko, A. Sirotkin, and P. Eugster. In ICNP'17.
  11. 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. [Formalization]
  12. Composing Middlebox and Traffic Engineering Policies in SDNs. With Y. Chang, S. Rao, and T. Rompf. At INFOCOM Workshop SWFAN'17.
  13. Programming Scalable Cloud Services with AEON. With B. Sang, M. Saeida Ardekani, S. Ravi, and P. Eugster. At Middleware'16. [Project Page]
  14. Consistency in 3D [TR]. With M. Shapiro and M. Saeida Ardekani. Invited contribution at CONCUR'16.
  15. Automatically Learning Shape Specifications. With He Zhu and S. Jagannathan. At PLDI'16. [Project Page]
  16. BASEL (Buffer mAnagement SpEcification Language). With K. Kogan, D. Menikkumbura, T. Noh, S. Nikolenko, and P. Eugster. At ANCS'16.
  17. Poling: SMT Aided Linearizability Proofs. With He Zhu and S. Jagannathan. At CAV'15. [Project Page]
  18. Cooking the Books: Formalizing JMM Implementation Recipes. With J. Vitek and S. Jagannathan. At ECOOP'15. [Video] [Extended Version]
  19. Atomicity Refinement for Verified Compilation. With S. Jagannathan, V. Laporte, D. Pichardie and J. Vitek. Appeared at TOPLAS'14. Presented at PLDI'14. [Formalization]
  20. Studying Operational Models of Relaxed Concurrency. At TGC'13.
  21. Quarantining Weakness: Compositional Reasoning Under Relaxed Memory Models. With R. Jagadeesan, J. Riely and C. Pitcher. At ESOP'13.
  22. Relaxed Semantics of Concurrent Programming Languages (long version). With Gérard Boudol and Bernard Serpette. At Express/SOS'12. [Simulator]
  23. Brookes is Relaxed, Almost! With Radha Jagadeesan and James Riely. At FoSSaCS'12.
  24. Operational Semantics for Relaxed Memory Models (Thesis), 2010.
  25. A Theory of Speculative Computation. With Gérard Boudol. At ESOP'10.
  26. Relaxed Memory Models: An Operational Approach. With Gérard Boudol. At POPL'09.
  27. BicolanoMT: A Formalization of Multi-threaded Java at Bytecode Level. With Marieke Huisman. At Bytecode'08. [Formalization]
  28. The Java Memory Model: A Formal Explanation. With Marieke Huisman. In Verification and Analysis of Multi-threaded Java-like Programs (VAMP'07). [Formalization]