Gustavo Petri

Publication Activity (10 Years)

Years Active: 2009-2024
Publications (10 Years): 28

Top Topics

Transactional Properties

Referential Integrity

Buffer Management

Top Venues

Proc. ACM Program. Lang.

Publications

Edgard Schiebelbein, Saalik Hatia, Annette Bieniusa, Gustavo Petri, Carla Ferreira, Marc Shapiro
Models for Storage in Database Backends. CoRR (2024)
Edgard Schiebelbein, Saalik Hatia, Annette Bieniusa, Carla Ferreira, Gustavo Petri, Marc Shapiro
Models for Storage in Database Backends. PaPoC@EuroSys (2024)
Anthony C. J. Fox, Gareth Stockwell, Shale Xiong, Hanno Becker, Dominic P. Mulligan, Gustavo Petri, Nathan Chong
A Verification Methodology for the Arm® Confidential Computing Architecture: From a Secure Specification to Safe Implementations. Proc. ACM Program. Lang. 7 (OOPSLA1) (2023)
Chao Wang, Gustavo Petri, Yi Lv, Teng Long, Zhiming Liu
Decidability of Liveness for Concurrent Objects on the TSO Memory Model. SETTA (2022)
Chao Wang, Gustavo Petri, Yi Lv, Teng Long, Zhiming Liu
Decidability of Liveness on the TSO Memory Model. CoRR (2021)
Yao Hsiao, Dominic P. Mulligan, Nikos Nikoleris, Gustavo Petri, Caroline Trippel
Synthesizing Formal Models of Hardware from RTL for Efficient Verification of Memory Model Implementations. MICRO (2021)
Dominic P. Mulligan, Gustavo Petri, Nick Spinale, Gareth Stockwell, Hugo J. M. Vincent
Confidential Computing - a brave new world. SEED (2021)
Bo Sang, Pierre-Louis Roman, Patrick Eugster, Hui Lu, Srivatsan Ravi, Gustavo Petri
PLASMA: programmable elasticity for stateful cloud computing applications. EuroSys (2020)
Bo Sang, Patrick Eugster, Gustavo Petri, Srivatsan Ravi, Pierre-Louis Roman
Scalable and serializable networked multi-actor programming. Proc. ACM Program. Lang. 4 (OOPSLA) (2020)
Tanakorn Leesatapornwongsa, Aritra Sengupta, Masoud Saeida Ardekani, Gustavo Petri, Cesar A. Stuardo
Transactuations: Where Transactions Meet the Physical World. ACM Trans. Comput. Syst. 36 (4) (2020)
Kirill Kogan, Danushka Menikkumbura, Gustavo Petri, Youngtae Noh, Sergey I. Nikolenko, Alexander Sirotkin, Patrick Eugster
Towards Software-Defined Buffer Management. IEEE/ACM Trans. Netw. 28 (5) (2020)
Sreeja S. Nair, Gustavo Petri, Marc Shapiro
Proving the Safety of Highly-Available Distributed Objects. ESOP (2020)
Constantin Enea, Suha Orhun Mutluergil, Gustavo Petri, Chao Wang
Replication-Aware Linearizability. CoRR (2019)
Chao Wang, Constantin Enea, Suha Orhun Mutluergil, Gustavo Petri
Replication-aware linearizability. PLDI (2019)
Sreeja Nair, Gustavo Petri, Marc Shapiro
Invariant Safety for Distributed Applications. CoRR (2019)
Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek
Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology. J. Autom. Reason. 63 (2) (2019)
Bo Sang, Gustavo Petri, Masoud Saeida Ardekani, Srivatsan Ravi, Patrick Eugster
Programming Scalable Cloud Services with AEON. CoRR (2019)
Sreeja S. Nair, Gustavo Petri, Marc Shapiro
Invariant Safety for Distributed Applications. PaPoC@EuroSys (2019)
Marc Shapiro, Annette Bieniusa, Peter Zeller, Gustavo Petri
Ensuring referential integrity under causal consistency. CoRR (2018)
Marc Shapiro, Annette Bieniusa, Peter Zeller, Gustavo Petri
Ensuring referential integrity under causal consistency. PaPoC@EuroSys (2018)
Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek
Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology. ITP (2017)
Kirill Kogan, Danushka Menikkumbura, Gustavo Petri, Yangtae Noh, Sergey I. Nikolenko, Alexander Sirotkin, Patrick Eugster
A programmable buffer management platform. ICNP (2017)
Yiyang Chang, Gustavo Petri, Sanjay G. Rao, Tiark Rompf
Composing middlebox and traffic engineering policies in SDNs. INFOCOM Workshops (2017)
Bo Sang, Srivatsan Ravi, Gustavo Petri, Mahsa Najafzadeh, Masoud Saeida Ardekani, Patrick Eugster
Programmable Elasticity for Actor-based Cloud Applications. PLOS@SOSP (2017)
Kirill Kogan, Danushka Menikkumbura, Gustavo Petri, Youngtae Noh, Sergey I. Nikolenko, Patrick Eugster
BASEL (Buffer mAnagement SpEcification Language). ANCS (2016)
Marc Shapiro, Masoud Saeida Ardekani, Gustavo Petri
Consistency in 3D. CONCUR (2016)
He Zhu, Gustavo Petri, Suresh Jagannathan
Automatically learning shape specifications. PLDI (2016)
Bo Sang, Gustavo Petri, Masoud Saeida Ardekani, Srivatsan Ravi, Patrick Eugster
Programming Scalable Cloud Services with AEON. Middleware (2016)
Gustavo Petri, Jan Vitek, Suresh Jagannathan
Cooking the Books: Formalizing JMM Implementation Recipes. ECOOP (2015)
He Zhu, Gustavo Petri, Suresh Jagannathan
Poling: SMT Aided Linearizability Proofs. CAV (2) (2015)
Kirill Kogan, Danushka Menikkumbura, Gustavo Petri, Youngtae Noh, Sergey I. Nikolenko, Patrick Eugster
BASEL (Buffering Architecture SpEcification Language). CoRR (2015)
Suresh Jagannathan, Gustavo Petri, Jan Vitek, David Pichardie, Vincent Laporte
Atomicity refinement for verified compilation. PLDI (2014)
Suresh Jagannathan, Vincent Laporte, Gustavo Petri, David Pichardie, Jan Vitek
Atomicity Refinement for Verified Compilation. ACM Trans. Program. Lang. Syst. 36 (2) (2014)
Gustavo Petri
Studying Operational Models of Relaxed Concurrency. TGC (2013)
Radha Jagadeesan, Gustavo Petri, Corin Pitcher, James Riely
Quarantining Weakness - Compositional Reasoning under Relaxed Memory Models (Extended Abstract). ESOP (2013)
Gérard Boudol, Gustavo Petri, Bernard P. Serpette
Relaxed Operational Semantics of Concurrent Programming Languages EXPRESS/SOS (2012)
Radha Jagadeesan, Gustavo Petri, James Riely
Brookes Is Relaxed, Almost! FoSSaCS (2012)
Gérard Boudol, Gustavo Petri
A Theory of Speculative Computation. ESOP (2010)
Gérard Boudol, Gustavo Petri
Relaxed memory models: an operational approach. POPL (2009)