Travelled to:1 × India
Collaborated with:Z.Shao David Costanzo X.(.Wu X.Yuan J.Yang Hao Chen 0023 J.Koenig T.Ramananandro E.Zhai R.Piskac Xun Lao X.Wang Joshua Lockerman M.L.0001 L.Rieg J.Kim M.Yoon S.Weng H.Zhang Y.Guo Jieung Kim V.Sjöberg
Talks about:abstract (3) concurr (2) certifi (2) verif (2) layer (2) end (2) preemptiv (1) interrupt (1) composit (1) virtual (1)
Person: Ronghui Gu
DBLP: Gu:Ronghui
Contributed to:
2015
2018
2017
201620182020Wrote 7 papers:
- POPL-2015-GuKRSWWZG #abstraction #specification
- Deep Specifications and Certified Abstraction Layers (RG, JK, TR, ZS, X(W, SCW, HZ, YG), pp. 595–608.
- CAV-2018-YuanYG #concurrent #partial order
- Partial Order Aware Concurrency Sampling (XY, JY, RG), pp. 317–335.
- OOPSLA-2017-ZhaiPGLW #correlation #in the cloud
- An auditing language for preventing correlated failures in the cloud (EZ, RP, RG, XL, XW), p. 28.
- PLDI-2016-ChenWSLG #composition #kernel #towards #verification
- Toward compositional verification of interruptible OS kernels and device drivers (HC0, X(W, ZS, JL, RG), pp. 431–447.
- PLDI-2016-CostanzoSG #assembly #c #data flow #security #source code #verification
- End-to-end verification of information-flow security for C and assembly programs (DC, ZS, RG), pp. 648–664.
- PLDI-2018-GuSKWKS0CR #abstraction #concurrent
- Certified concurrent abstraction layers (RG, ZS, JK, X(W, JK, VS, HC0, DC, TR), pp. 646–661.
- POPL-2020-LiuRSGCKY #abstraction #timeline #verification
- Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation (ML0, LR, ZS, RG, DC, JEK, MKY), p. 31.