Travelled to:7 × USA
Collaborated with:K.Elphinstone ∅ L.Ryzhyk Y.Shi B.Blackham G.Klein P.Chubb H.Jung H.Han A.D.Fekete H.Y.Yeom I.Kuz E.L.Sueur G.Keller T.C.Murray S.Amani L.O'Connor Z.Chen J.Keys B.Mirla A.Raghunath M.Vij T.Sewell J.Andronick D.Cock P.Derrin D.Elkaduwe K.Engelhardt R.Kolanski M.Norrish H.Tuch S.Winwood Alex Hixon C.Rizkallah Joel Beeren Y.Nagashima J.Lim Joseph Tuong
Talks about:system (3) verif (3) verifi (2) formal (2) driver (2) devic (2) file (2) sel (2) microkernel (1) implement (1)
Person: Gernot Heiser
DBLP: Heiser:Gernot
Contributed to:
2013
2013
2013
2013
2011
201120092016Wrote 9 papers:
- OOPSLA-2013-ShiBH #optimisation #using
- Code optimizations using formally verified properties (YS, BB, GH), pp. 427–442.
- PLOS-2013-KellerMAOCRKH #exclamation #file system #verification
- File systems deserve verification too! (GK, TCM, SA, LO, ZC, LR, GK, GH), p. 7.
- SIGMOD-2013-JungHFHY #multi #scalability
- A scalable lock manager for multicores (HJ, HH, ADF, GH, HYY), pp. 73–84.
- SOSP-2013-ElphinstoneH #kernel #question #what
- From L3 to seL4 what have we learnt in 20 years of L4 microkernels? (KE, GH), pp. 133–150.
- ASPLOS-2011-RyzhykKMRVH #hardware #reliability #reuse #verification
- Improved device driver reliability through hardware verification reuse (LR, JK, BM, AR, MV, GH), pp. 133–144.
- DAC-2011-Heiser #embedded #question #why
- Virtualizing embedded systems: why bother? (GH), pp. 901–905.
- SOSP-2009-KleinEHACDEEKNSTW #kernel #named #verification
- seL4: formal verification of an OS kernel (GK, KE, GH, JA, DC, PD, DE, KE, RK, MN, TS, HT, SW), pp. 207–220.
- SOSP-2009-RyzhykCKSH #automation #synthesis
- Automatic device driver synthesis with termite (LR, PC, IK, ELS, GH), pp. 73–86.
- ASPLOS-2016-AmaniHCRCOBNLST #file system #implementation #named #verification
- CoGENT: Verifying High-Assurance File System Implementations (SA, AH, ZC, CR, PC, LO, JB, YN, JL, TS, JT, GK, TCM, GK, GH), pp. 175–188.