THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT!

,-------------------.
|     PREAMBLE      |
`-------------------'

@preamble{ "\providecommand{\noopsort}[1]{}
           \providecommand{\url}{\error{The bib files now require the
           `url' package!}}"
}

,-------------------.
|  BIBTEX ENTRIES   |
`-------------------'

  @inproceedings{Blackham_SCRH_11,
    author           = {Blackham, Bernard and Shi, Yao and Chattopadhyay, Sudipta and Roychoudhury, Abhik and Heiser, Gernot},
    month            = nov,
    pages            = {339-348},
    year             = {2011},
    title            = {Timing Analysis of a Protected Operating System Kernel},
    booktitle        = {IEEE Real-Time Systems Symposium},
    address          = {Vienna, Austria}
  }

  @inproceedings{Blackham_SH_12,
    author           = {Blackham, Bernard and Shi, Yao and Heiser, Gernot},
    month            = apr,
    pages            = {323-336},
    year             = {2012},
    title            = {Improving Interrupt Response Time in a Verifiable Protected Microkernel},
    booktitle        = {EuroSys},
    address          = {Bern, Switzerland}
  }

@inproceedings{Boyton_09,
  address =       {Aachen, Germany},
  author =        {Andrew Boyton},
  booktitle =     {Proceedings of the 4th Workshop on Systems Software
                   Verification},
  editor =        {Gerwin Klein and Ralf Huuck and Bastian Schlich},
  month =         oct,
  pages =         {25--44},
  publisher =     {Elsevier},
  series =        {Electronic Notes in Computer Science},
  title =         {A Verified Shared Capability Model},
  volume =        {254},
  year =          {2009},
}

@inproceedings{Cock_KS_08,
  address =       {Montreal, Canada},
  author =        {David Cock and Gerwin Klein and Thomas Sewell},
  booktitle =     {Proceedings of the 21st International Conference on
                   Theorem Proving in Higher Order Logics},
  editor =        {Otmane Ait Mohamed and C\'{e}sar Mu{\~{n}}oz and
                   Sofi\`{e}ne Tahar},
  month =         aug,
  pages =         {167--182},
  publisher =     {Springer-Verlag},
  series =        {Lecture Notes in Computer Science},
  title =         {Secure Microkernels, State Monads and Scalable
                   Refinement},
  volume =        {5170},
  year =          {2008},
  doi =           {10.1007/978-3-540-71067-7\_16},
}

@inproceedings{Derrin_EKCC_06,
  address =       {Portland, OR, USA},
  author =        {Philip Derrin and Kevin Elphinstone and Gerwin Klein and
                   David Cock and Manuel M. T. Chakravarty},
  booktitle =     {Proceedings of the ACM SIGPLAN Haskell Workshop},
  month =         sep,
  title =         {Running the Manual: An Approach to High-Assurance
                   Microkernel Development},
  year =          {2006},
}

@inproceedings{Elkaduwe_GE_08,
  address =       {Toronto, Canada},
  author =        {Dhammika Elkaduwe and Gerwin Klein and
                   Kevin Elphinstone},
  booktitle =     {Proceedings of Verified Software: Theories, Tools and
                   Experiments 2008},
  editor =        {Jim Woodcock and Natarajan Shankar},
  month =         oct,
  pages =         {99--114},
  publisher =     {Springer-Verlag},
  series =        {Lecture Notes in Computer Science},
  title =         {Verified Protection Model of the {seL4} Microkernel},
  volume =        {5295},
  year =          {2008},
}

@inproceedings{Klein_EHACDEEKNSTW_09,
  address =       {Big Sky, MT, USA},
  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},
  booktitle =     {Proceedings of the 22nd ACM Symposium on Operating
                   Systems Principles},
  month =         oct,
  pages =         {207--220},
  publisher =     {ACM},
  title =         {{seL4}: Formal Verification of an {OS} Kernel},
  year =          {2009},
  doi =           {10.1145/1629575.1629596},
}

  @inproceedings{Murray_MBGBSLGK_13,
    author           = {Murray, Toby and Matichuk, Daniel and Brassil, Matthew and Gammie, Peter and Bourke, Timothy and
                        Seefried, Sean and Lewis, Corey and Gao, Xin and Klein, Gerwin},
    month            = may,
    pages            = {415-429},
    year             = {2013},
    title            = {{seL4}: from General Purpose to a Proof of Information Flow Enforcement},
    booktitle        = {IEEE Symposium on Security \& Privacy},
    address          = {San Francisco, CA}
  }

  @inproceedings{Sewell_WGMAK_11,
    author           = {Sewell, Thomas and Winwood, Simon and Gammie, Peter and Murray, Toby and Andronick, June and Klein,
                        Gerwin},
    pages            = {325-340},
    month            = aug,
    editor           = {{Marko van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk}},
    year             = {2011},
    title            = {{seL4} Enforces Integrity},
    booktitle        = {Interactive Theorem Proving (ITP)},
    address          = {Nijmegen, The Netherlands}
  }

@inproceedings{Tuch_KN_07,
  address =       {Nice, France},
  author =        {Harvey Tuch and Gerwin Klein and Michael Norrish},
  booktitle =     {Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium
                   on Principles of Programming Languages},
  editor =        {Martin Hofmann and Matthias Felleisen},
  month =         jan,
  pages =         {97--108},
  publisher =     {ACM},
  title =         {Types, Bytes, and Separation Logic},
  year =          {2007},
}

@inproceedings{Winwood_KSACN_09,
  address =       {Munich, Germany},
  author =        {Simon Winwood and Gerwin Klein and Thomas Sewell and
                   June Andronick and David Cock and Michael Norrish},
  booktitle =     {Proceedings of the 22nd International Conference on
                   Theorem Proving in Higher Order Logics},
  editor =        {Stefan Berghofer and Tobias Nipkow and
                   Christian Urban and Makarius Wenzel},
  month =         aug,
  pages =         {500--515},
  publisher =     {Springer-Verlag},
  series =        {Lecture Notes in Computer Science},
  title =         {Mind the Gap: A Verification Framework for Low-Level
                   {C}},
  volume =        {5674},
  year =          {2009},
}

@manual{extra:vtd,
  author =        {{Intel Corporation}},
  month =         feb,
  note =
  {\url{http://download.intel.com/technology/computing/vptech/Intel(r)_VT_for_Direct_IO.pdf}},
  title =         {Intel Virtualization Technology for Directed I/O ---
                   Architecture Specification},
  year =          {2011},
}

@book{Shanley:PCISA,
  author =        {Tom Shanley and Don Anderson},
  publisher =     {Mindshare, Inc.},
  title =         {PCI System Architecture},
  year =          {1999},
}

@mastersthesis{Palande:M,
  address =       {Amsterdam},
  author =        {Ameya Palande},
  month =         jan,
  school =        {Vrije Universiteit},
  type =          {Masters Thesis},
  title =         {Capability-based Secure {DMA} in {seL4}},
  year =          {2009},
}

@inproceedings{Baumann_BDHIPRSS_09,
  address =       {Big Sky, MT, USA},
  author =        {Andrew Baumann and Paul Barham and
                   Pierre-Evariste Dagand and Tim Harris and
                   Rebecca Isaacs and Simon Peter and Timothy Roscoe and
                   Adrian Sch{\"u}pbach and Akhilesh Singhania},
  booktitle =     {Proceedings of the 22nd ACM Symposium on Operating
                   Systems Principles},
  month =         oct,
  publisher =     {ACM},
  title =         {The multikernel: A new {OS} architecture for scalable
                   multicore systems},
  year =          {2009},
}

@inproceedings{vonTessin_10,
  address =       {Edinburgh, UK},
  author =        {von Tessin, Michael},
  booktitle =     {Proceedings of the 6th International Verification
                   Workshop},
  editor =        {Markus Aderhold and Serge Autexier and Heiko Mantel},
  month =         jul,
  pages =         {110--125},
  publisher =     {EasyChair},
  series =        {EasyChair Proceedings in Computing},
  title =         {Towards High-Assurance Multiprocessor Virtualisation},
  volume =        {3},
  year =          {2010},
  issn =          {2040-557X},
}

@inproceedings{vonTessin_12,
  address =       {Bern, Switzerland},
  author =        {von Tessin, Michael},
  booktitle =     {Proceedings of the 2nd Workshop on Systems for Future
                   Multi-core Architectures},
  month =         apr,
  title =         {The Clustered Multikernel: An Approach to Formal
                   Verification of Multiprocessor {OS} Kernels},
  year =          {2012},
}

