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