@article{Klein_09,
  author={Gerwin Klein},
  title={Operating System Verification --- An Overview},
  journal={S\={a}dhan\={a}},
  publisher={Springer},
  year=2009,
  volume=34,
  number=1,
  month=Feb,
  pages={27--69},
}

@inproceedings{Elkaduwe_KE_08,
  author =      {Dhammika Elkaduwe and Gerwin Klein and Kevin Elphinstone},
  title =       {Verified Protection Model of the {seL4} Microkernel},
  booktitle = {Second IFIP Working Conference on
  Verified Software: Theories, Tools, and Experiments (VSTTE 2008)},
  editor =      {Jim Woodcock and Natarajan Shankar},
  address =     {Toronto, Canada},
  publisher =   {Springer},
  year =         2008,
  month =        oct,
  series =      {LNCS},
  pages =     {99--114},
  volume =    5295,
}

@InProceedings{Kolanski_Klein_08,
  author =    {Rafal Kolanski and Gerwin Klein},
  title =     {Mapped Separation Logic},
  booktitle = {Second IFIP Working Conference on
  Verified Software: Theories, Tools, and Experiments (VSTTE 2008)},
  editor =    {Jim Woodcock and Natarajan Shankar},
  series =    {LNCS},
  publisher =  {Springer},
  volume =    5295,
  pages =	 {15--29},
  year =      {2008},
  isbn =	 {978-3-540-87872-8},
  address =   {Toronto, Canada},
  month =     Oct,
}

@InProceedings{Cock_KS_08,
  author = {David Cock and Gerwin Klein and Thomas Sewell},
  title = {Secure Microkernels, State Monads and Scalable Refinement},
  booktitle = {Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs'08)},
  year = {2008},
  editor = {Cesar Munoz and Otmane Ait},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  note = {To appear}
}

@InProceedings{Tuch_KN_07,
  author =    {Harvey Tuch and Gerwin Klein and Michael Norrish},
  title =     {Types, Bytes, and Separation Logic},
  booktitle = {Proc.\ 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'07)},
  pages =     {97-108},
  year =      {2007},
  editor =    {Martin Hofmann and Matthias Felleisen},
  address =   {Nice, France},
  month =     Jan,
}

@inproceedings{ElphinstoneKK-06,
  author =    {Kevin Elphinstone and Gerwin Klein and Rafal Kolanski},
  title =     {Formalising a High-Performance Microkernel},
  booktitle = {Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06)},
  series =    {Microsoft Research Technical Report MSR-TR-2006-117},
  year =      {2006},
  editor =    {Rustan Leino},
  address =   {Seattle, USA},
  month =     Aug,
  pages =     {1-7},
}

@inproceedings{WinwoodKC-06,
  author =       {Simon Winwood and Gerwin Klein and Manuel M. T. Chakravarty},
  title =        {On the automated synthesis of proof-carrying temporal reference monitors},
  booktitle =    {International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 06)},
  year =      {2007},
  series =    {LNCS},
  volume =    4407,
  editor =    {Germán Puebla},
  address =   {Italy},
  pages =     {111--126},
  publisher = {Springer}
}

@inproceedings{KolanskiK-06,
  author =       {Rafal Kolanski and Gerwin Klein},
  title =        {Formalising the L4 microkernel API},
  booktitle =    {Computing: The Australasian Theory Symposium (CATS 06)},
  year =      {2006},
  editor =    {Barry Jay and Joachim Gudmundsson},
  address =   {Hobart, Australia},
  month =     Jan,
  pages =     {53--68},
  series =    {Conferences in Research and Practice in Information Technology},
  volume =    {51}
}

@inproceedings{TuchK-05,
  author =       {Harvey Tuch and Gerwin Klein},
  title =        {A Unified Memory Model for Pointers},
  booktitle =    {12th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-12)},
  year =      {2005},
  editor =    {Geoff Sutcliffe and Andrei Voronkov},
  address =   {Jamaica},
  month =     Dec,
  pages =     {474--488},
  series =    {Lecture Notes in Computer Science},
  volume =    {3835},
}

@inproceedings{TuchKN-05,
  author =       {Harvey Tuch and Gerwin Klein and Gernot Heiser},
  title =        {OS Verification --- Now!},
  booktitle =    {Proc.\ 10th Workshop on Hot Topics in Operating Systems (HotOS X)},
  year =      {2005},
  editor =    {Margo Seltzer},
}

@inproceedings{KleinHuuck05,
  author =       {Gerwin Klein and Ralf Huuck},
  title =        {High Assurance System Software},
  booktitle =    {Proc.\ 10th Australian Workshop on Safety Critical Systems and Software (SCS'05)},
  year =         {2005},
  editor =       {Tony Cant},
  volume =       {55},
  series =       {Conferences in Research and Practice in Information Technology},
  address =      {Sydney, Australia},
  month =        Aug,
  publisher =    {Australian Computer Society, Inc},
  note  =        {9 pages}
}

@proceedings{OSV04,
  title = 	 {Proc.\ NICTA Formal Methods Workshop on Operating Systems Verification},
  year = 	 {2004},
  editor = 	 {Gerwin Klein},
  organization = {NICTA Technical Report 0401005T-1},
  address = 	 {Sydney, Australia},
  publisher =    {National ICT Australia},
}

@inproceedings{TuchKleinOSV04,
  author = 	 {Harvey Tuch and Gerwin Klein},
  title = 	 {Verifying the {L4} Virtual Memory Subsystem},
  booktitle = 	 {Proc.\ NICTA Formal Methods Workshop on Operating Systems Verification},
  pages = 	 {73--97},
  year = 	 {2004},
  editor = 	 {Gerwin Klein},
  organization = {NICTA Technical Report 0401005T-1},
  publisher =    {National ICT Australia},
}

@InProceedings{KleinTuchTPHOLs04,
  author = 	 {Gerwin Klein and Harvey Tuch},
  title = 	 {Towards Verified Virtual Memory in L4},
  booktitle = 	 {TPHOLs Emerging Trends '04},
  pages = 	 {16 pages},
  year = 	 {2004},
  editor = 	 {Konrad Slind},
  address = 	 {Park City, Utah, USA},
  month = 	 Sep,
  note = 	 {available from \url{http://www.cse.unsw.edu.au/~kleing/papers/towards-verified-vm.pdf}},
}

@inproceedings{WildmoserNKN-TCS04,
author={Martin Wildmoser and Tobias Nipkow and Gerwin Klein and Sebastian Nanz},
title={Prototyping Proof Carrying Code},
booktitle={Proc.\ 3rd IFIP Int.\ Conf.\ Theoretical Computer Science (TCS 2004)},
year=2004}

@techreport{KleinN04,
  author={Gerwin Klein and Tobias Nipkow},
  title={A Machine-Checked Model for a {Java}-Like Language, Virtual Machine and Compiler},
  institution={National ICT Australia},
  number={0400001T.1},
  address={Sydney},
  month=mar,
  year=2004
}

@inproceedings{BrandlK-HCI99,
  author =    {Alfons Brandl and Gerwin Klein},
  title =     {{FormGen}: A Generator for Adaptive Forms Based on {EasyGUI}},
  booktitle = {Human-Computer Interaction: Ergonomics and Userinterfaces. Proc.\ HCI'99},
  pages =     {1172--1176},
  year =      1999,
  editor =    {H. Bullinger and J. Ziegler},
  volume =    {1},
  publisher = {Lawrence Erlbaum Associates, Inc.},
}


@MastersThesis{Klein99,
  author =    {Gerwin Klein},
  title =     {Generating Graphical Editors for Graph-like Datastructures},
  school = {Lehrstuhl f{\"u}r Informatik II, Technische Universit{\"a}t M{\"u}nchen},
  year =      {1999},
  abstract =  {Many modern applications favor one or more graphical diagram editors,
of which -- despite their different look \& feel and problem domains -- on a
closer look many have very similar functionality.  Examples are
UML class diagrams, finite automata, electronic circuit diagrams, or
network charts. Their similarity is, that in an
abstract way they all work on, edit and display a graph.

These editors and diagram viewers are mostly implemented by hand.
Although this work is not very often done from scratch but rather
with the help of some object oriented framework, it remains a complex
task with usually high development costs.

This diploma thesis focuses on how the development and maintenance
cost for this kind of graphical editors can be reduced. The problem is
addressed in three steps:

We analyze example applications, extracting and structuring
classes of requirements for graph editors to examine and clearly
define the problem domain.

We develop a description language that allows to define and fully
specify a graph editor in an abstract way. These specifications are
thought to support the analysis and design phase in the development
process. Compared to a full natural language description or a complete
implementation, they are compact, easy to read, easy to communicate
and easy to change.

We take a generative approach to automatically reach a full
implementation of the graph editor defined by such specifications and
discuss important aspects like the integration of generated code into
existing applications and full customizability of generated
editors in more detail.} 
}

@Article{KleinS-JLP04,
  author =  {Gerwin Klein and Martin Strecker},
  title =   {Verified {B}ytecode {V}erification and Type-Certifying {C}ompilation},
  journal = {Journal of Logic and Algebraic Programming},
  volume = 58,
  number = {1--2},
  pages = {27--60},
  year =    2004,
}

@article{KleinW-JAR03,
  author =  {Gerwin Klein and Martin Wildmoser},
  title =   {Verified Bytecode Subroutines},
  journal = {Journal of Automated Reasoning},
  year =    2003,
  volume = 30,
  number = {3--4},
  pages = {363--398},
  editor = {Tobias Nipkow},
}


@InProceedings{KleinW-TPHOLS03,
  author =       {Gerwin Klein and Martin Wildmoser},
  title =        {Verified Bytecode Subroutines},
  booktitle =    {Proceedings of Theorem Proving in Higher Order Logics},
  pages =        {55--70},
  year =         {2003},
  editor =       {David Basin and Burkhard Wolff},
  volume =       {2758},
  series =       {Lecture Notes in Computer Science},
}

@article{KleinN-CCPE01,
  author = {Gerwin Klein and Tobias Nipkow},
  title = {Verified Lightweight Bytecode Verification},
  journal = {Concurrency and Computation: Practice and Experience},
  editor = {S. Eisenbach and G. T. Leavens},
  publisher = {John Wiley and Sons},
  volume = 13,
  number = 13,
  pages = {1133-1151},
  year = 2001,
}

@inproceedings{KleinN00,
  author = {Gerwin Klein and Tobias Nipkow},
  title = {Verified Lightweight Bytecode Verification},
  booktitle = {Proc.\ 2nd {ECOOP} Workshop on Formal Techniques for {Java} Programs},
  year = {2000},
  publisher = {Fernuniversit{{\"a}t} Hagen},
  editor = {S. Drossopoulou and S. Eisenbach and B. Jacobs and 
            G. T. Leavens and P. M{\"u}ller and A. Poetzsch-Heffter},
  organization = {TR 269},
  pages = {35--42}
}

@article{KleinN-TCS02,
  author={Gerwin Klein and Tobias Nipkow},
  title={Verified Bytecode Verifiers},
  journal={Theoretical Computer Science},
  year="2002",
  pages="583--626",
  volume={298},
  number={3},
  editor={F. Honsell and M. Miculan},
}

@Manual{Klein-JFlex,
  title =     {{JFlex}: the fast lexical analyzer generator for {Java}},
  author =    {Gerwin Klein},
  year =      {1998},
  note =      {[\url{http://jflex.de}]},
}

@phdthesis{Klein-PhD,
  author =       {Gerwin Klein},
  title =        {Verified Java Bytecode Verification},
  school =  {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
  year =         {2003},
}

@Misc{Klein-Spock,
  author =    {Gerwin Klein and Michael Rott and Siegfried Sch{\"a}fler and Stephan Wimmer},
  title =     {{Schnelle Algorithmen f{\"u}r d{\"u}nnbesetze Polynome}},
  howpublished = {Institut f{\"u}r Mathematik, Technische Universit{\"a}t M{\"u}nchen},
  year =      {1997},
}


@Misc{Klein-EasyGUI,
  author =    {Gerwin Klein},
  title =     {{Die objekt-orientierte Bedienoberfl{\"a}chenbibliothek EasyGUI}},
  howpublished = {Lehrstuhl f{\"u}r Informatik II, Technische Universit{\"a}t M{\"u}nchen},
  year =      {1997},
  note =      {Systementwicklungsprojekt}
}

@Article{Heiser_EKKP_07,
  author =       {Gernot Heiser and Kevin Elphinstone and Ihor Kuz and
                  Gerwin Klein and Stefan M. Petters},
  title =        {Towards Trustworthy Computing Systems: Taking
                  Microkernels to the Next Level},
  journal =      {Operating Systems Review},
  year =         2007,
  month =        jul,
  volume =       {41},
  number =       {4},
  pages =        {3--11},
}

@InProceedings{Elphinstone_KDRH_07,
  author =       {Kevin Elphinstone and Gerwin Klein and Philip Derrin
                  and Timothy Roscoe and Gernot Heiser},
  title =        {Towards a Practical, Verified Kernel},
  booktitle =    {Proc.\ 11th Workshop on Hot Topics in Operating Systems},
  year =         2007,
  pages =        6,
  address =      {San Diego, CA, USA},
  month =        may,
  note =         {Online proceedings at \url{http://www.usenix.org/events/hotos07/tech/}}
}

@InProceedings{Meng_PK_07,
  author =       {Jia Meng and Lawrence C. Paulson and Gerwin Klein},
  title =        {A Termination Checker for Isabelle Hoare Logic},
  booktitle =    {4th International Verification Workshop - VERIFY'07},
  editor =       {Bernhard Beckert},
  pages =        {104--118},
  year =         {2007},
  address =      {Bremen, Germany},
  month =        jul,
  volume =       {259},
  series =       {CEUR Workshop Proceedings},
  issn =         {1613-0073},
}

@InProceedings{Kolanski_Klein_09,
    author =    {Rafal Kolanski and Gerwin Klein},
    title =     {Types, Maps and Separation Logic},
    booktitle = {Proc.\ 22nd TPHOLs},
    editor =    {Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel},
    year =         {2009},
    address =      {Munich, Germany},
    pages =        {276--292},
    month =        Aug,
    series =       {Lecture Notes in Computer Science},
    volume =       {5674},
    publisher =    {Springer},
}

@InProceedings{Winwood_KSACN_09,
    author =    {Simon Winwood and Gerwin Klein and Thomas Sewell and 
                 June Andronick and David Cock and Michael Norrish},
    title =     {Mind the Gap: A Verification Framework for Low-Level {C}},
    booktitle = {Proc.\ 22nd TPHOLs},
    editor =    {Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel},
    year =         {2009},
    address =      {Munich, Germany},
    pages =        {500-515},
    month =        Aug,
    series =       {Lecture Notes in Computer Science},
    volume =       {5674},
    publisher =    {Springer},
}

@InProceedings{Klein_DE_09,
    author =    {Gerwin Klein and Philip Derrin and Kevin Elphinstone},
    title =     {Experience report: seL4 --- Formally Verifying a High-Performance Microkernel},
    booktitle = {Proc.\ 2009 ACM SIGPLAN International Conference on Functional Programming (ICFP)},
    year =         {2009},
    pages =        {91--96},
    month =        Aug,
    publisher =    {ACM},
}

@InProceedings{Klein_EHACDEEKNSTW_09,
    author =  {Gerwin Klein 
    and Kevin Elphinstone 
    and Gernot Heiser
    and June Andronick 
    and David Cock
    and Philip Derrin
    and Dhammika Elkaduwe
    and Kai Engelhardt
    and Rafal Kolanski
    and Michael Norrish
    and Thomas Sewell
    and Harvey Tuch
    and Simon Winwood},
    title =        {{seL4}: Formal Verification of an {OS} Kernel},
    booktitle =    {Proc.\ 22nd ACM Symposium on Operating Systems Principles (SOSP)},
    publisher =    {ACM},
    year =         {2009},
    address =      {Big Sky, MT, USA},
    month =        oct,
    pages =        {207--220}
}

@proceedings{svv09,
  editor = {Ralf Huuck and Gerwin Klein and Bastian Schlich},
  title = {Proc.\ 4th International Workshop on System Software Verification (SSV09)},
  series = {ENTCS},
  volume = 254,
  publisher = {Elsevier},
  year = 2009,
}

@article{Klein_09:login,
  author = 	 {Gerwin Klein},
  title = 	 {Correct OS Kernel? Proof? Done!},
  journal =  {USENIX ;login:},
  year = 	 2009,
  volume = 	 34,
  number = 	 6,
  pages = 	 {28--34},
  month = 	 dec,
  publisher = {USENIX},
}

@InProceedings{Klein_10,
    author =    {Gerwin Klein},
    title =     {A Formally Verified OS Kernel. Now What?},
    booktitle = {Proc.\ First International Conference on Interactive Theorem Proving (ITP'2010)},
    editor =    {Matt Kaufmann and Lawrence C Paulson},
    year =         {2010},
    address =      {Edinburgh, UK},
    pages =        {1--7},
    month =        Jul,
    series =       {Lecture Notes in Computer Science},
    volume =       {6172},
    publisher =    {Springer},
}

@InProceedings{Klein_10b,
    author =    {Gerwin Klein},
    title =     {The L4.verified Project - Next Steps},
    booktitle = {Proc.\ 3rd International Conference on Verified Software: Theories, Tools, Experiments (VSTTE'2010)},
    editor =    {Gary Leavens and Peter O'Hearn and Sriram Rajamani},
    year =      {2010},
    address =   {Edinburgh, UK},
    pages =     {86--96},
    month =     Aug,
    series =    {Lecture Notes in Computer Science},
    volume =    {6217},
    publisher =  {Springer},
}

@inbook{Klein_SW_10,
    author =    {Gerwin Klein and Thomas Sewell and Simon Winwood},
    title =     {Refinement in the formal verification of seL4},
    booktitle = {Design and Verification of Microprocessor Systems for High-Assurance Applications},
    editor =    {David S. Hardin},
    pages =     {323--339},
    month =     Mar,
    year =      {2010},
    publisher = {Springer},
    doi =       {10.1007/978-1-4419-1539-9_11},
}