Relaxed memory models: an operational approach. - Gérard Boudol; Gustavo Petri (POPL, 2009)

A Theory of Speculative Computation. - Gérard Boudol; Gustavo Petri (ESOP, 2010)

Brookes Is Relaxed, Almost! - Radha Jagadeesan; Gustavo Petri; James Riely (FoSSaCS, 2012)

Relaxed Operational Semantics of Concurrent Programming Languages - Gérard Boudol; Gustavo Petri; Bernard P. Serpette (EXPRESS/SOS, 2012)

Quarantining Weakness - Compositional Reasoning under Relaxed Memory Models (Extended Abstract). - Radha Jagadeesan; Gustavo Petri; Corin Pitcher; James Riely (ESOP, 2013)

Studying Operational Models of Relaxed Concurrency. - Gustavo Petri (TGC, 2013)

Atomicity Refinement for Verified Compilation. - Suresh Jagannathan; Vincent Laporte; Gustavo Petri; David Pichardie; Jan Vitek (ACM Trans. Program. Lang. Syst., 2014)

Poling: SMT Aided Linearizability Proofs. - He Zhu 001; Gustavo Petri; Suresh Jagannathan (CAV (2), 2015)

Cooking the Books: Formalizing JMM Implementation Recipes. - Gustavo Petri; Jan Vitek; Suresh Jagannathan (ECOOP, 2015)

BASEL (Buffering Architecture SpEcification Language). - Kirill Kogan; Danushka Menikkumbura; Gustavo Petri; Youngtae Noh; Sergey I. Nikolenko; Patrick Eugster (CoRR, 2015)

BASEL (Buffer mAnagement SpEcification Language). - Kirill Kogan; Danushka Menikkumbura; Gustavo Petri; Youngtae Noh; Sergey I. Nikolenko; Patrick Eugster (ANCS, 2016)

Consistency in 3D. - Marc Shapiro 001; Masoud Saeida Ardekani; Gustavo Petri (CONCUR, 2016)

Programming Scalable Cloud Services with AEON. - Bo Sang; Gustavo Petri; Masoud Saeida Ardekani; Srivatsan Ravi; Patrick Eugster (Middleware, 2016)

Automatically learning shape specifications. - He Zhu 001; Gustavo Petri; Suresh Jagannathan (PLDI, 2016)

A programmable buffer management platform. - Kirill Kogan; Danushka Menikkumbura; Gustavo Petri; Yangtae Noh; Sergey I. Nikolenko; Alexander Sirotkin 001; Patrick Eugster (ICNP, 2017)

Composing middlebox and traffic engineering policies in SDNs. - Yiyang Chang; Gustavo Petri; Sanjay G. Rao; Tiark Rompf (INFOCOM Workshops, 2017)

Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology. - Yannick Zakowski; David Cachera; Delphine Demange; Gustavo Petri; David Pichardie; Suresh Jagannathan; Jan Vitek (ITP, 2017)

Programmable Elasticity for Actor-based Cloud Applications. - Bo Sang; Srivatsan Ravi; Gustavo Petri; Mahsa Najafzadeh; Masoud Saeida Ardekani; Patrick Eugster (PLOS@SOSP, 2017)

Ensuring referential integrity under causal consistency. - Marc Shapiro 001; Annette Bieniusa; Peter Zeller 001; Gustavo Petri (PaPoC@EuroSys, 2018)

Transactuations: Where Transactions Meet the Physical World. - Tanakorn Leesatapornwongsa; Aritra Sengupta; Masoud Saeida Ardekani; Gustavo Petri; Cesar A. Stuardo (ACM Trans. Comput. Syst., 2018)

Invariant Safety for Distributed Applications. - Sreeja S. Nair; Gustavo Petri; Marc Shapiro 001 (PaPoC@EuroSys, 2019)

Replication-aware linearizability. - Chao Wang 069; Constantin Enea; Suha Orhun Mutluergil; Gustavo Petri (PLDI, 2019)

Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology. - Yannick Zakowski; David Cachera; Delphine Demange; Gustavo Petri; David Pichardie; Suresh Jagannathan; Jan Vitek (J. Autom. Reason., 2019)

Proving the Safety of Highly-Available Distributed Objects. - Sreeja S. Nair; Gustavo Petri; Marc Shapiro 001 (ESOP, 2020)

PLASMA: programmable elasticity for stateful cloud computing applications. - Bo Sang; Pierre-Louis Roman; Patrick Eugster; Hui Lu 001; Srivatsan Ravi; Gustavo Petri (EuroSys, 2020)

Scalable and serializable networked multi-actor programming. - Bo Sang; Patrick Eugster; Gustavo Petri; Srivatsan Ravi; Pierre-Louis Roman (Proc. ACM Program. Lang., 2020)

Towards Software-Defined Buffer Management. - Kirill Kogan; Danushka Menikkumbura; Gustavo Petri; Youngtae Noh; Sergey I. Nikolenko; Alexander Sirotkin 001; Patrick Eugster (IEEE/ACM Trans. Netw., 2020)

Synthesizing Formal Models of Hardware from RTL for Efficient Verification of Memory Model Implementations. - Yao Hsiao; Dominic P. Mulligan; Nikos Nikoleris; Gustavo Petri; Caroline Trippel (MICRO, 2021)

Confidential Computing - a brave new world. - Dominic P. Mulligan; Gustavo Petri; Nick Spinale; Gareth Stockwell; Hugo J. M. Vincent (SEED, 2021)

Decidability of Liveness on the TSO Memory Model. - Chao Wang 069; Gustavo Petri; Yi Lv; Teng Long; Zhiming Liu 001 (CoRR, 2021)

Decidability of Liveness for Concurrent Objects on the TSO Memory Model. - Chao Wang 069; Gustavo Petri; Yi Lv; Teng Long; Zhiming Liu 001 (SETTA, 2022)

A Verification Methodology for the Arm® Confidential Computing Architecture: From a Secure Specification to Safe Implementations. - Anthony C. J. Fox; Gareth Stockwell; Shale Xiong; Hanno Becker; Dominic P. Mulligan; Gustavo Petri; Nathan Chong (Proc. ACM Program. Lang., 2023)

RTL2MμPATH: Multi-μPATH Synthesis with Applications to Hardware Security Verification. - Yao Hsiao; Nikos Nikoleris; Artem Khyzha; Dominic P. Mulligan; Gustavo Petri; Christopher W. Fletcher; Caroline Trippel (MICRO, 2024)

Models for Storage in Database Backends. - Edgard Schiebelbein; Saalik Hatia; Annette Bieniusa; Carla Ferreira 001; Gustavo Petri; Marc Shapiro 001 (PaPoC@EuroSys, 2024)

Universal Construction for Linearizable but Not Strongly Linearizable Concurrent Objects. - Chao Wang 069; Peng Wu 002; Gustavo Petri; Qiaowen Jia; Youlin He; Yi Lv; Zhiming Liu 001 (SETTA, 2024)

Careful Whisper: Attestation for peer-to-peer Confidential Computing networks. - Ceren Kocaogullar; Gustavo Petri; Dominic P. Mulligan; Derek Miller; Hugo J. M. Vincent; Shale Xiong; Alastair R. Beresford (CoRR, 2025)