@misc(ARM_manual,
 title        = {ARM Infocenter},
 url          = {http://infocenter.arm.com/},
)
@misc(eChronos,
 title        = {The eChronos OS},
 url          = {http://echronos.systems},
)
@article(Feng_SGD_09,
 author       = {Xinyu Feng and Zhong Shao and Yu Guo and Yuan Dong},
 year         = {2009},
 title        = {Certifying low-level programs with hardware interrupts and preemptive threads},
 journal      = {Journal of Automated Reasoning},
 volume       = {42},
 number       = {2-4},
 pages        = {301--347},
 doi          = {10.1007/s10817-009-9118-9},
)
@article(Ferreira_HQ_12,
 author       = {Joao F Ferreira and Cristian Gherghina and Guanhua He and Shengchao Qin and Wei-Ngan Chin},
 year         = {2014},
 title        = {Automated verification of the FreeRTOS scheduler in HIP/SLEEK},
 journal      = {International Journal on Software Tools for Technology Transfer},
 volume       = {16},
 number       = {4},
 pages        = {381--397},
 doi          = {10.1109/TASE.2012.45},
)
@article(Hansen_72,
 author       = {Per Brinch Hansen},
 year         = {1972},
 title        = {Structured Multiprogramming},
 journal      = {Communications of the ACM},
 volume       = {15},
 pages        = {574--578},
 doi          = {10.1145/361454.361473},
)
@article(Hoare_69,
 author       = {C. A. R. Hoare},
 year         = {1969},
 title        = {An Axiomatic Basis for Computer Programming},
 journal      = {Communications of the ACM},
 volume       = {12},
 pages        = {576--580},
 doi          = {10.1145/363235.363259},
)
@article(Hoare_74,
 author       = {C. A. R. Hoare},
 year         = {1974},
 title        = {Monitors: An Operating System Structuring Concept},
 journal      = {Communications of the ACM},
 volume       = {17},
 pages        = {549--557},
 doi          = {10.1145/355620.361161},
)
@inproceedings(Huang_11,
 author       = {Yanhong Huang and Yongxin Zhao and Longfei Zhu and Qin Li and Huibiao Zhu and Jianqi Shi},
 year         = {2011},
 title        = {Modeling and verifying the code-level OSEK/VDX operating system with CSP},
 booktitle    = {Theoretical Aspects of Software Engineering (TASE), 2011 Fifth International Symposium on},
 organization = {IEEE},
 pages        = {142--149},
 doi          = {10.1109/TASE.2011.11},
)
@article(Jones_83,
 author       = {C. B. Jones},
 year         = {1983},
 title        = {Tentative steps towards a development method for interfering programs},
 journal      = {ACM Transactions on Programming Languages and Systems},
 volume       = {5},
 number       = {4},
 pages        = {596--619},
 doi          = {10.1145/69575.69577},
)
@article(Klein_09,
 author       = {Gerwin Klein},
 year         = {2009},
 title        = {Operating System Verification --- An Overview},
 journal      = {S\={a}dhan\={a}},
 volume       = {34},
 number       = {1},
 pages        = {27--69},
 doi          = {10.1007/s12046-009-0002-4},
)
@article(Klein_AEMSKH_14,
 author       = {Gerwin Klein and June Andronick and Kevin Elphinstone and Toby Murray and Thomas Sewell and Rafal Kolanski and Gernot Heiser},
 year         = {2014},
 title        = {Comprehensive Formal Verification of an {OS} Microkernel},
 journal      = {ACM Transactions on Computer Systems},
 volume       = {32},
 number       = {1},
 pages        = {2:1--2:70},
 doi          = {10.1145/2560537},
)
@book(Nipkow_PW:Isabelle,
 author       = {Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
 year         = {2002},
 title        = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
 volume       = {2283},
 doi          = {10.1007/3-540-45949-9},
)
@article(OHearn_07,
 author       = {Peter W. OHearn},
 year         = {2007},
 title        = {Resources, Concurrency, and Local Reasoning},
 journal      = {Theor. Comput. Sci.},
 volume       = {375},
 number       = {1-3},
 pages        = {271--307},
 doi          = {10.1016/j.tcs.2006.12.035},
)
@article(Owicki_Gries_76,
 author       = {Susan Owicki and David Gries},
 year         = {1976},
 title        = {An axiomatic proof technique for parallel programs},
 journal      = {Acta Informatica},
 volume       = {6},
 pages        = {319--340},
 doi          = {10.1007/BF00268134},
)
@phdthesis(Prensa:PhD,
 author       = {Prensa Nieto, Leonor},
 year         = {2002},
 title        = {Verification of parallel programs with the {Owicki-Gries} and rely-guarantee methods in {Isabelle/HOL}},
 school       = {Technische Universit{\"a}t M{\"u}nchen},
)
@incollection(Richards_10,
 author       = {Raymond J. Richards},
 year         = {2010},
 title        = {Modeling and Security Analysis of a Commercial Real-Time Operating System Kernel},
 pages        = {301--322},
 publisher    = {Springer US},
 doi          = {10.1007/978-1-4419-1539-9\_10},
)
@inproceedings(Yang_Hawblitzel_10,
 author       = {Jean Yang and Chris Hawblitzel},
 year         = {2010},
 title        = {Safe to the last instruction: automated verification of a type-safe operating system},
 address      = {Toronto, Ontario, Canada},
 pages        = {99--110},
 doi          = {10.1145/1806596.1806610},
)