BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Petri:Gustavo

Contributed to:

CAV 20152015
ECOOP 20152015
PLDI 20142014
ESOP 20132013
FOSSACS 20122012
ESOP 20102010
POPL 20092009
PLDI 20162016
PLDI 20192019

Wrote 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.
Replication-aware linearizability (CW, CE, SOM, GP), pp. 980–993.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.