@inproceedings(Cock_KS_08,
 author       = "David Cock and Gerwin Klein and Thomas Sewell",
 year         = "2008",
 title        = "Secure Microkernels, State Monads and Scalable Refinement",
 editor       = "Otmane Ait Mohamed and C\'{e}sar Mu{\~{n}}oz and Sofi\`{e}ne Tahar",
 booktitle    = "21st TPHOLs",
 series       = "LNCS",
 volume       = "5170",
 publisher    = "Springer-Verlag",
 address      = "Montreal, Canada",
 pages        = "167--182",
)
@inproceedings(Cohen_DHLMSST_09,
 author       = "Ernie Cohen and Markus Dahlweid and Mark Hillebrand and Dirk Leinenbach and Micha{\l } Moskal and Thomas Santen and Wolfram Schulte and Stephan Tobies",
 year         = "2009",
 title        = "{VCC}: A Practical System for Verifying Concurrent {C}",
 editor       = "Stefan Berghofer and Tobias Nipkow and Christian Urban and Markus Wenzel",
 booktitle    = "22nd TPHOLs",
 series       = "LNCS",
 volume       = "5674",
 publisher    = "Springer-Verlag",
 address      = "Munich, Germany",
 pages        = "23--42",
)
@article(Hoare:1983:ABC:357980.358001,
 author       = "C. A. R. Hoare",
 year         = "1983",
 title        = "An axiomatic basis for computer programming",
 journal      = "Commun. ACM",
 volume       = "26",
 number       = "1",
 pages        = "53--56",
 doi          = "10.1145/357980.358001",
)
@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",
 year         = "2009",
 title        = "{seL4}: Formal Verification of an {OS} Kernel",
 booktitle    = "22nd SOSP",
 publisher    = "ACM",
 address      = "Big Sky, MT, USA",
 pages        = "207--220",
)
@incollection(Mossakowski_TSLGS_08,
 author       = "Till Mossakowski and Lutz Schröder and Sergey Goncharov",
 year         = "2008",
 title        = "A Generic Complete Dynamic Logic for Reasoning About Purity and Effects",
 editor       = "José Fiadeiro and Paola Inverardi",
 booktitle    = "Fundamental Approaches to Software Engineering",
 series       = "Lecture Notes in Computer Science",
 volume       = "4961",
 publisher    = "Springer Berlin / Heidelberg",
 pages        = "199--214",
 doi          = "10.1007/978-3-540-78743-3\_15",
)
@inproceedings(Murray_MBGK_12,
 author       = "Toby Murray and Daniel Matichuk and Matthew Brassil and Peter Gammie and Gerwin Klein",
 year         = "2012",
 title        = "Noninterference for Operating System Kernels",
 booktitle    = "2nd Int. Conf. Certified Programs \& Proofs",
 note         = "To appear",
)
@inproceedings(Sewell_WGMAK,
 author       = "Thomas Sewell and Simon Winwood and Peter Gammie and Toby Murray and June Andronick and Gerwin Klein",
 year         = "2011",
 title        = "{seL4} Enforces Integrity",
 editor       = "Marko C. J. D. van Eekelen and Herman Geuvers and Julien Schmaltz and Freek Wiedijk",
 booktitle    = "2nd ITP",
 series       = "LNCS",
 volume       = "6898",
 publisher    = "Springer-Verlag",
 address      = "Nijmegen, The Netherlands",
 pages        = "325--340",
 doi          = "10.1007/978-3-642-22863-6\_24",
)
@incollection(Sprenger_B_07,
 author       = "Christoph Sprenger and David Basin",
 year         = "2007",
 title        = "A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols",
 editor       = "Klaus Schneider and Jens Brandt",
 booktitle    = "Theorem Proving in Higher Order Logics",
 series       = "Lecture Notes in Computer Science",
 volume       = "4732",
 publisher    = "Springer Berlin / Heidelberg",
 pages        = "302--318",
 doi          = "10.1007/978-3-540-74591-4\_23",
)
@incollection(Swierstra_09,
 author       = "Wouter Swierstra",
 year         = "2009",
 title        = "A Hoare Logic for the State Monad",
 editor       = "Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel",
 booktitle    = "Theorem Proving in Higher Order Logics",
 series       = "Lecture Notes in Computer Science",
 volume       = "5674",
 publisher    = "Springer Berlin / Heidelberg",
 pages        = "440--451",
 doi          = "10.1007/978-3-642-03359-9\_30",
)