Gustavo Petri

According to our database, Gustavo Petri authored at least 35 papers between 2009 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

Universal Construction for Linearizable but Not Strongly Linearizable Concurrent Objects.

Chao Wang, Peng Wu, Gustavo Petri, Qiaowen Jia, Youlin He, Yi Lv, Zhiming Liu

Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2024

Models for Storage in Database Backends.

Edgard Schiebelbein, Saalik Hatia, Annette Bieniusa, Carla Ferreira, Gustavo Petri, Marc Shapiro

Proceedings of the 11th Workshop on Principles and Practice of Consistency for Distributed Data, 2024

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

Proceedings of the 57th IEEE/ACM International Symposium on Microarchitecture, 2024

2023

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., April, 2023

2022

Decidability of Liveness for Concurrent Objects on the TSO Memory Model.

Chao Wang, Gustavo Petri, Yi Lv, Teng Long, Zhiming Liu

Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2022

2021

Decidability of Liveness on the TSO Memory Model.

Chao Wang, Gustavo Petri, Yi Lv, Teng Long, Zhiming Liu

CoRR, 2021

Confidential Computing - a brave new world.

Dominic P. Mulligan, Gustavo Petri, Nick Spinale, Gareth Stockwell, Hugo J. M. Vincent

Proceedings of the 2021 International Symposium on Secure and Private Execution Environment Design (SEED), 2021

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

Proceedings of the MICRO '21: 54th Annual IEEE/ACM International Symposium on Microarchitecture, 2021

2020

Towards Software-Defined Buffer Management.

Kirill Kogan, Danushka Menikkumbura, Gustavo Petri, Youngtae Noh, Sergey I. Nikolenko, Alexander Sirotkin, Patrick Eugster

IEEE/ACM Trans. Netw., 2020

Scalable and serializable networked multi-actor programming.

Bo Sang, Patrick Eugster, Gustavo Petri, Srivatsan Ravi, Pierre-Louis Roman

Proc. ACM Program. Lang., 2020

PLASMA: programmable elasticity for stateful cloud computing applications.

Bo Sang, Pierre-Louis Roman, Patrick Eugster, Hui Lu, Srivatsan Ravi, Gustavo Petri

Proceedings of the EuroSys '20: Fifteenth EuroSys Conference 2020, 2020

Proving the Safety of Highly-Available Distributed Objects.

Sreeja S. Nair, Gustavo Petri, Marc Shapiro

Proceedings of the Programming Languages and Systems, 2020

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

Replication-aware linearizability.

Chao Wang, Constantin Enea, Suha Orhun Mutluergil, Gustavo Petri

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Invariant Safety for Distributed Applications.

Sreeja S. Nair, Gustavo Petri, Marc Shapiro

Proceedings of the 6th Workshop on Principles and Practice of Consistency for Distributed Data, 2019

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

Ensuring referential integrity under causal consistency.

Marc Shapiro, Annette Bieniusa, Peter Zeller, Gustavo Petri

Proceedings of the 5th Workshop on the Principles and Practice of Consistency for Distributed Data, 2018

2017

Programmable Elasticity for Actor-based Cloud Applications.

Bo Sang, Srivatsan Ravi, Gustavo Petri, Mahsa Najafzadeh, Masoud Saeida Ardekani, Patrick Eugster

Proceedings of the 9th Workshop on Programming Languages and Operating Systems, 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

Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

Composing middlebox and traffic engineering policies in SDNs.

Yiyang Chang, Gustavo Petri, Sanjay G. Rao, Tiark Rompf

Proceedings of the 2017 IEEE Conference on Computer Communications Workshops, 2017

A programmable buffer management platform.

Kirill Kogan, Danushka Menikkumbura, Gustavo Petri, Yangtae Noh, Sergey I. Nikolenko, Alexander Sirotkin, Patrick Eugster

Proceedings of the 25th IEEE International Conference on Network Protocols, 2017

2016

Automatically learning shape specifications.

He Zhu, Gustavo Petri, Suresh Jagannathan

Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016

Programming Scalable Cloud Services with AEON.

Bo Sang, Gustavo Petri, Masoud Saeida Ardekani, Srivatsan Ravi, Patrick Eugster

Proceedings of the 17th International Middleware Conference, Trento, Italy, December 12, 2016

Consistency in 3D.

Marc Shapiro, Masoud Saeida Ardekani, Gustavo Petri

Proceedings of the 27th International Conference on Concurrency Theory, 2016

BASEL (Buffer mAnagement SpEcification Language).

Kirill Kogan, Danushka Menikkumbura, Gustavo Petri, Youngtae Noh, Sergey I. Nikolenko, Patrick Eugster

Proceedings of the 2016 Symposium on Architectures for Networking and Communications Systems, 2016

2015

BASEL (Buffering Architecture SpEcification Language).

Kirill Kogan, Danushka Menikkumbura, Gustavo Petri, Youngtae Noh, Sergey I. Nikolenko, Patrick Eugster

CoRR, 2015

Cooking the Books: Formalizing JMM Implementation Recipes.

Gustavo Petri, Jan Vitek, Suresh Jagannathan

Proceedings of the 29th European Conference on Object-Oriented Programming, 2015

Poling: SMT Aided Linearizability Proofs.

He Zhu, Gustavo Petri, Suresh Jagannathan

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014

Atomicity Refinement for Verified Compilation.

Suresh Jagannathan, Vincent Laporte, Gustavo Petri, David Pichardie, Jan Vitek

ACM Trans. Program. Lang. Syst., 2014

2013

Studying Operational Models of Relaxed Concurrency.

Gustavo Petri

Proceedings of the Trustworthy Global Computing - 8th International Symposium, 2013

Quarantining Weakness - Compositional Reasoning under Relaxed Memory Models (Extended Abstract).

Radha Jagadeesan, Gustavo Petri, Corin Pitcher, James Riely

Proceedings of the Programming Languages and Systems, 2013

2012

Relaxed Operational Semantics of Concurrent Programming Languages

Gérard Boudol, Gustavo Petri, Bernard P. Serpette

Proceedings of the Proceedings Combined 19th International Workshop on Expressiveness in Concurrency and 9th Workshop on Structured Operational Semantics, 2012

Brookes Is Relaxed, Almost!

Radha Jagadeesan, Gustavo Petri, James Riely

Proceedings of the Foundations of Software Science and Computational Structures, 2012

2010

A Theory of Speculative Computation.

Gérard Boudol, Gustavo Petri

Proceedings of the Programming Languages and Systems, 2010

2009

Relaxed memory models: an operational approach.

Gérard Boudol, Gustavo Petri

Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009