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 × 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 DBLP: Klein:Gerwin

Contributed to:

FM 20152015
ICSE 20152015
FM 20142014
PLDI 20142014
ICSE 20132013
PLDI 20132013
PLOS 20132013
ICSE 20122012
ICFP 20092009
SOSP 20092009
POPL 20072007
LOPSTR 20062006
HCI v1 19991999
Haskell 20062006
ASPLOS 20162016

Wrote 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.

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.