@inproceedings(Burrows-run-time-check,
 author       = "Michael Burrows and Stephen N. Freund and Janet L. Wiener",
 year         = "2003",
 title        = "Run-Time Type Checking for Binary Programs",
 editor       = "G{\"o}rel Hedin",
 booktitle    = "12th International Conference on Compiler Construction",
 series       = "LNCS",
 volume       = "2622",
 publisher    = "Springer",
 pages        = "90--105",
 doi          = "10.1007/3-540-36579-6\_7",
)
@manual(go,
 year         = "2012",
 title        = "The {Go} Programming Language Specification",
 url          = "http://golang.org/doc/go_spec.html",
 note         = "Retrieved June~15, 2012.",
)
@book(java,
 author       = "James Gosling and Bill Joy and Guy L. {Steele Jr.} and Gilad Bracha",
 year         = "2005",
 title        = "The {Java} Language Specification (3rd ed.)",
 publisher    = "Addison-Wesley",
)
@article(cyclone,
 author       = "D. Grossman and M. Hicks and T. Jim and G. Morrisett",
 year         = "2005",
 title        = "{Cyclone}: A Type-Safe Dialect of {C}",
 journal      = "C/C++ User's Journal",
 volume       = "23",
 number       = "1",
)
@inproceedings(DBLP:conf/csl/GurevichH92,
 author       = "Yuri Gurevich and James K. Huggins",
 year         = "1992",
 title        = "The Semantics of the {C} Programming Language",
 editor       = "Egon B{\"o}rger and Gerhard J{\"a}ger and Hans Kleine B{\"u}ning and Simone Martini and Michael M. Richter",
 booktitle    = "Computer Science Logic, CSL~'92",
 series       = "LNCS",
 volume       = "702",
 publisher    = "Springer",
 pages        = "274--308",
 doi          = "10.1007/3-540-56992-8\_17",
)
@incollection(vfiasco-types,
 author       = "M. Hohmuth and H. Tews",
 year         = "2003",
 title        = "The Semantics of {C++} Data Types: Towards Verifying low-level System Components",
 editor       = "David Basin and Burkhart Wolff",
 booktitle    = "Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003. Emerging Trends Proceedings",
 publisher    = "Universit\"at Freiburg",
 pages        = "127--144",
)
@inproceedings(vfiasco,
 author       = "M. Hohmuth and H. Tews",
 year         = "2005",
 title        = "The {VFiasco} approach for a verified operating system",
 editor       = "Andreas Gal and Christian W. Probst",
 booktitle    = "Proc.\ 2nd ECOOP Workshop on Programming Languages and Operating Systems (ECOOP-PLOS 2005)",
)
@manual(c11,
 organization = "ISO/IEC JTC1/SC22/WG14 C Standards Committee",
 year         = "2011",
 title        = "{\it Programming Languages---{C}}",
 note         = "{ISO/IEC} 9899:2011",
)
@manual(cpp11,
 organization = "ISO/IEC JTC1/SC22/WG21 C++ Standards Committee",
 year         = "2011",
 title        = "{\it Programming Languages---{C++}}",
 note         = "{ISO/IEC} 14882:2011",
)
@article(l4_verified,
 author       = "Gerwin Klein",
 year         = "2010",
 title        = "{seL4}: formal verification of an operating-system kernel",
 journal      = "Commun. ACM",
 volume       = "53",
 number       = "6",
 pages        = "107--115",
 doi          = "10.1145/1743546.1743574",
)
@inproceedings(Loginov-run-time-check,
 author       = "Alexey Loginov and Suan Hsi Yong and Susan Horwitz and Thomas W. Reps",
 year         = "2001",
 title        = "Debugging via Run-Time Type Checking",
 editor       = "Heinrich Hu{\ss }mann",
 booktitle    = "Fundamental Approaches to Software Engineering, FASE 2001",
 series       = "LNCS",
 volume       = "2029",
 publisher    = "Springer",
 pages        = "217--232",
 doi          = "10.1007/3-540-45314-8\_16",
)
@techreport(Norrish:CPP2008,
 author       = "Michael Norrish",
 year         = "2008",
 title        = "A Formal Semantics for {C++}",
 type         = "Technical Report",
 institution  = "NICTA",
 note         = "Available from \url {http://nicta.com.au/people/norrishm/attachments/bibliographies_and_papers/C-TR.pdf}. Retrieved June~15, 2012.",
)
@inproceedings(pvs2008,
 author       = "Sam Owre and Natarajan Shankar",
 year         = "2008",
 title        = "A Brief Overview of {PVS}",
 editor       = "Otmane A\"{\i }t Mohamed and C{\'e}sar Mu{\~n}oz and Sofi{\`e}ne Tahar",
 booktitle    = "Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008",
 series       = "LNCS",
 volume       = "5170",
 publisher    = "Springer",
 pages        = "22--27",
 doi          = "10.1007/978-3-540-71067-7\_5",
)
@inproceedings(bitc,
 author       = "Jonathan Shapiro",
 year         = "2006",
 title        = "Programming language challenges in systems codes: why systems programmers still use {C}, and what to do about it",
 editor       = "Christian W. Probst",
 booktitle    = "Proc.\ 3rd Workshop on Programming Languages and Operating Systems (PLOS 2006)",
 publisher    = "ACM",
 pages        = "9",
)
@article(tews:memory_peculiarities,
 author       = "Hendrik Tews and Marcus V{\"o}lp and Tjark Weber",
 year         = "2009",
 title        = "Formal Memory Models for the Verification of Low-Level Operating-System Code",
 journal      = "Journal of Automated Reasoning: Special Issue on Operating Systems Verification",
 volume       = "42",
 number       = "2--4",
 pages        = "189--227",
)
@techreport(tews08verification,
 author       = "Hendrik Tews and Tjark Weber and Marcus V{\"o}lp and Erik Poll and Marko van Eekelen and Peter van Rossum",
 year         = "2008",
 title        = "{Nova} Micro--Hypervisor Verification",
 type         = "Technical Report",
 number       = "ICIS--R08012",
 institution  = "Radboud University Nijmegen",
)
@inproceedings(tuch07types,
 author       = "Harvey Tuch and Gerwin Klein and Michael Norrish",
 year         = "2007",
 title        = "Types, Bytes, and Separation Logic",
 editor       = "Martin Hofmann and Matthias Felleisen",
 booktitle    = "Proc. 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007",
 publisher    = "ACM",
 pages        = "97--108",
 doi          = "10.1145/1190216.1190234",
)