Gustavo Petri

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