default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDGustavo Petri
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
[c26]Edgard Schiebelbein
, Saalik Hatia, Annette Bieniusa, Carla Ferreira, Gustavo Petri, Marc Shapiro:
Models for Storage in Database Backends. PaPoC@EuroSys 2024: 58-66- [i8]Edgard Schiebelbein, Saalik Hatia, Annette Bieniusa, Gustavo Petri, Carla Ferreira, Marc Shapiro:
Models for Storage in Database Backends. CoRR abs/2403.11716 (2024) - [i7]Yao Hsiao, Nikos Nikoleris, Artem Khyzha, Dominic P. Mulligan, Gustavo Petri, Christopher W. Fletcher, Caroline Trippel:
RTL2MμPATH: Multi-μPATH Synthesis with Applications to Hardware Security Verification. CoRR abs/2409.19478 (2024) - 2023
- [j6]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): 376-405 (2023) - 2022
- [c25]Chao Wang, Gustavo Petri, Yi Lv, Teng Long, Zhiming Liu:
Decidability of Liveness for Concurrent Objects on the TSO Memory Model. SETTA 2022: 149-165 - 2021
- [c24]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: 679-694 - [c23]Dominic P. Mulligan, Gustavo Petri, Nick Spinale, Gareth Stockwell, Hugo J. M. Vincent:
Confidential Computing - a brave new world. SEED 2021: 132-138 - [i6]Chao Wang, Gustavo Petri, Yi Lv, Teng Long, Zhiming Liu:
Decidability of Liveness on the TSO Memory Model. CoRR abs/2107.09930 (2021) - 2020
- [j5]Bo Sang, Patrick Eugster, Gustavo Petri, Srivatsan Ravi, Pierre-Louis Roman:
Scalable and serializable networked multi-actor programming. Proc. ACM Program. Lang. 4(OOPSLA): 198:1-198:30 (2020) - [j4]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): 2337-2349 (2020) - [c22]Sreeja S. Nair, Gustavo Petri, Marc Shapiro:
Proving the Safety of Highly-Available Distributed Objects. ESOP 2020: 544-571 - [c21]Bo Sang, Pierre-Louis Roman, Patrick Eugster, Hui Lu, Srivatsan Ravi, Gustavo Petri:
PLASMA: programmable elasticity for stateful cloud computing applications. EuroSys 2020: 42:1-42:15
2010 – 2019
- 2019
- [j3]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): 489-515 (2019) - [c20]Sreeja S. Nair, Gustavo Petri, Marc Shapiro:
Invariant Safety for Distributed Applications. PaPoC@EuroSys 2019: 4:1-4:7 - [c19]Chao Wang, Constantin Enea, Suha Orhun Mutluergil, Gustavo Petri:
Replication-aware linearizability. PLDI 2019: 980-993 - [i5]Sreeja Nair, Gustavo Petri, Marc Shapiro:
Invariant Safety for Distributed Applications. CoRR abs/1903.02759 (2019) - [i4]Constantin Enea, Suha Orhun Mutluergil, Gustavo Petri, Chao Wang:
Replication-Aware Linearizability. CoRR abs/1903.06560 (2019) - [i3]Bo Sang, Gustavo Petri, Masoud Saeida Ardekani, Srivatsan Ravi, Patrick Eugster:
Programming Scalable Cloud Services with AEON. CoRR abs/1912.03506 (2019) - 2018
- [j2]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): 13:1-13:31 (2018) - [c18]Marc Shapiro, Annette Bieniusa, Peter Zeller, Gustavo Petri:
Ensuring referential integrity under causal consistency. PaPoC@EuroSys 2018: 1:1-1:5 - [i2]Marc Shapiro, Annette Bieniusa, Peter Zeller, Gustavo Petri:
Ensuring referential integrity under causal consistency. CoRR abs/1803.03482 (2018) - 2017
- [c17]Kirill Kogan, Danushka Menikkumbura, Gustavo Petri, Yangtae Noh, Sergey I. Nikolenko, Alexander Sirotkin, Patrick Eugster:
A programmable buffer management platform. ICNP 2017: 1-10 - [c16]Yiyang Chang, Gustavo Petri, Sanjay G. Rao, Tiark Rompf:
Composing middlebox and traffic engineering policies in SDNs. INFOCOM Workshops 2017: 396-401 - [c15]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: 496-513 - [c14]Bo Sang, Srivatsan Ravi, Gustavo Petri, Mahsa Najafzadeh, Masoud Saeida Ardekani, Patrick Eugster:
Programmable Elasticity for Actor-based Cloud Applications. PLOS@SOSP 2017: 15-21 - 2016
- [c13]Kirill Kogan, Danushka Menikkumbura, Gustavo Petri, Youngtae Noh, Sergey I. Nikolenko, Patrick Eugster:
BASEL (Buffer mAnagement SpEcification Language). ANCS 2016: 69-74 - [c12]Marc Shapiro, Masoud Saeida Ardekani, Gustavo Petri:
Consistency in 3D. CONCUR 2016: 3:1-3:14 - [c11]Bo Sang, Gustavo Petri, Masoud Saeida Ardekani, Srivatsan Ravi, Patrick Eugster:
Programming Scalable Cloud Services with AEON. Middleware 2016: 16 - [c10]He Zhu, Gustavo Petri, Suresh Jagannathan:
Automatically learning shape specifications. PLDI 2016: 491-507 - 2015
- [c9]He Zhu, Gustavo Petri, Suresh Jagannathan:
Poling: SMT Aided Linearizability Proofs. CAV (2) 2015: 3-19 - [c8]Gustavo Petri, Jan Vitek, Suresh Jagannathan:
Cooking the Books: Formalizing JMM Implementation Recipes. ECOOP 2015: 445-469 - [i1]Kirill Kogan, Danushka Menikkumbura, Gustavo Petri, Youngtae Noh, Sergey I. Nikolenko, Patrick Eugster:
BASEL (Buffering Architecture SpEcification Language). CoRR abs/1510.04235 (2015) - 2014
- [j1]Suresh Jagannathan, Vincent Laporte, Gustavo Petri, David Pichardie, Jan Vitek:
Atomicity Refinement for Verified Compilation. ACM Trans. Program. Lang. Syst. 36(2): 6:1-6:30 (2014) - [c7]Suresh Jagannathan, Gustavo Petri, Jan Vitek, David Pichardie, Vincent Laporte:
Atomicity refinement for verified compilation. PLDI 2014: 27 - 2013
- [c6]Radha Jagadeesan, Gustavo Petri, Corin Pitcher, James Riely:
Quarantining Weakness - Compositional Reasoning under Relaxed Memory Models (Extended Abstract). ESOP 2013: 492-511 - [c5]Gustavo Petri:
Studying Operational Models of Relaxed Concurrency. TGC 2013: 254-272 - 2012
- [c4]Radha Jagadeesan, Gustavo Petri, James Riely:
Brookes Is Relaxed, Almost! FoSSaCS 2012: 180-194 - [c3]Gérard Boudol, Gustavo Petri, Bernard P. Serpette:
Relaxed Operational Semantics of Concurrent Programming Languages. EXPRESS/SOS 2012: 19-33 - 2010
- [c2]Gérard Boudol, Gustavo Petri:
A Theory of Speculative Computation. ESOP 2010: 165-184
2000 – 2009
- 2009
- [c1]Gérard Boudol, Gustavo Petri:
Relaxed memory models: an operational approach. POPL 2009: 392-403
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-18 19:31 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
