Travelled to:1 × France
1 × Germany
1 × Norway
1 × Singapore
1 × Switzerland
2 × Italy
2 × United Kingdom
4 × USA
Collaborated with:J.Andronick P.Derrin K.Elphinstone M.M.T.Chakravarty M.Fernandez I.Kuz ∅ A.Brandl T.C.Murray D.R.Jeffery M.Staples M.Norrish H.Tuch S.Winwood R.Kolanski T.A.L.Sewell M.O.Myreen J.Lim D.Cock G.Heiser D.Greenaway G.Keller S.Amani L.O'Connor Z.Chen D.Matichuk T.Sewell H.Zhang L.Zhu C.Lewis L.Bass L.Ryzhyk D.Elkaduwe K.Engelhardt Alex Hixon C.Rizkallah P.Chubb Joel Beeren Y.Nagashima Joseph Tuong
Talks about:formal (6) verif (6) verifi (4) high (3) code (3) microkernel (2) toward (2) system (2) kernel (2) proof (2)
Person: Gerwin Klein
DBLP: Klein:Gerwin
Contributed to:
2015
20152014
201420132013
20132012
2009
2009
2007
2006
1999
2006
2016Wrote 16 papers:
- FM-2015-FernandezAKK #automation #verification
- Automated Verification of RPC Stub Code (MF, JA, GK, IK), pp. 273–290.
- ICSE-v1-2015-MatichukMAJKS #empirical #formal method #towards #verification
- Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification (DM, TCM, JA, DRJ, GK, MS), pp. 722–732.
- FM-2014-Klein #proving
- Proof Engineering Considered Essential (GK), pp. 16–21.
- PLDI-2014-GreenawayLAK #c #verification
- Don’t sweat the small stuff: formal verification of C code without the pain (DG, JL, JA, GK), p. 45.
- ICSE-2013-StaplesKKLAMJB #specification
- Formal specifications better than function points for code sizing (MS, RK, GK, CL, JA, TCM, DRJ, LB), pp. 1257–1260.
- PLDI-2013-SewellMK #kernel #validation
- Translation validation for a verified OS kernel (TALS, MOM, GK), pp. 471–482.
- PLOS-2013-FernandezKKA #component #framework #platform #towards
- Towards a verified component platform (MF, IK, GK, JA), p. 7.
- PLOS-2013-KellerMAOCRKH #exclamation #file system #verification
- File systems deserve verification too! (GK, TCM, SA, LO, ZC, LR, GK, GH), p. 7.
- ICSE-2012-AndronickJKKSZZ #perspective #process #scalability #verification
- Large-scale formal verification in practice: A process perspective (JA, DRJ, GK, RK, MS, HZ, LZ), pp. 1002–1011.
- ICFP-2009-KleinDE #case study #experience #kernel #verification
- Experience report: seL4: formally verifying a high-performance microkernel (GK, PD, KE), pp. 91–96.
- 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.
- POPL-2007-TuchKN #logic
- Types, bytes, and separation logic (HT, GK, MN), pp. 97–108.
- LOPSTR-2006-WinwoodKC #automation #monitoring #on the #synthesis
- On the Automated Synthesis of Proof-Carrying Temporal Reference Monitors (SW, GK, MMTC), pp. 111–126.
- HCI-EI-1999-BrandlK #adaptation #generative #named
- FormGen: A Generator for Adaptive Forms Based on EasyGUI (AB, GK), pp. 1172–1176.
- Haskell-2006-DerrinEKCC #approach #development #kernel
- Running the manual: an approach to high-assurance microkernel development (PD, KE, GK, DC, MMTC), pp. 60–71.
- 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.