Travelled to:1 × Cyprus
1 × Czech Republic
1 × Estonia
1 × Italy
1 × United Kingdom
2 × USA
Collaborated with:S.Jagannathan G.Boudol R.Jagadeesan J.Riely J.Vitek H.Zhu He Zhu 0001 C.Pitcher C.Wang C.Enea S.O.Mutluergil D.Pichardie V.Laporte
Talks about:relax (3) lineariz (2) memori (2) model (2) quarantin (1) implement (1) composit (1) approach (1) automat (1) verifi (1)
Person: Gustavo Petri
DBLP: Petri:Gustavo
Contributed to:
2015
2015
2014
2013
20122010
200920162019Wrote 9 papers:
- CAV-2015-ZhuPJ #named #proving #smt
- Poling: SMT Aided Linearizability Proofs (HZ, GP, SJ), pp. 3–19.
- ECOOP-2015-PetriVJ #formal method #implementation
- Cooking the Books: Formalizing JMM Implementation Recipes (GP, JV, SJ), pp. 445–469.
- PLDI-2014-JagannathanPVPL #compilation #refinement
- Atomicity refinement for verified compilation (SJ, GP, JV, DP, VL), p. 5.
- ESOP-2013-JagadeesanPPR #composition #memory management #modelling #reasoning
- Quarantining Weakness — Compositional Reasoning under Relaxed Memory Models (RJ, GP, CP, JR), pp. 492–511.
- FoSSaCS-2012-JagadeesanPR #exclamation
- Brookes Is Relaxed, Almost! (RJ, GP, JR), pp. 180–194.
- ESOP-2010-BoudolP #formal method
- A Theory of Speculative Computation (GB, GP), pp. 165–184.
- POPL-2009-BoudolP #approach #memory management #modelling
- Relaxed memory models: an operational approach (GB, GP), pp. 392–403.
- PLDI-2016-ZhuPJ #automation #learning #specification
- Automatically learning shape specifications (HZ0, GP, SJ), pp. 491–507.
- PLDI-2019-WangEMP
- Replication-aware linearizability (CW, CE, SOM, GP), pp. 980–993.