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