This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.

Gerwin Klein

Gerwin Klein: seL4 from several distances - the kernel's functional-correctness proof, its groundwork (a Java-like language model; types, bytes and separation logic), and retrospectives on deployment.

seL4 in Australia: From Research to Real-World Trustworthy Systems

Gernot Heiser and others (2020) · Communications of the ACM · Association for Computing Machinery

Formal Reasoning Under Cached Address Translation

Hira Taqdees Syeda and others (2020) · Journal of Automated Reasoning · Springer Science and Business Media LLC

Backwards and Forwards with Separation Logic

Callum Bannister and others (2018) · 9th International Conference on Interactive Theorem Proving (ITP) · Springer

Formally verified software in the real world

Gerwin Klein and others (2018) · Communications of the ACM · Association for Computing Machinery

Program Verification in the Presence of Cached Address Translation

Hira Taqdees Syeda and others (2018) · Springer International Publishing

Reasoning about Translation Lookaside Buffers

Hira Syeda and others (2017) · EPiC series in computing

An empirical research agenda for understanding formal methods productivity

Ross Jeffery and others (2014) · Information and Software Technology · Elsevier BV

Comprehensive formal verification of an OS microkernel

Gerwin Klein and others (2014) · ACM Transactions on Computer Systems · Association for Computing Machinery

Formally Verified System Initialisation

Andrew Boyton and others (2013) · Lecture notes in computer science · Springer Science+Business Media

seL4: From General Purpose to a Proof of Information Flow Enforcement

Toby Murray and others (2013) · Proceedings - IEEE Symposium on Security and Privacy/Proceedings of the ... IEEE Symposium on Security and Privacy · IEEE Computer Society

Translation validation for a verified OS kernel

Thomas Arthur Leck Sewell and others (2013) · Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation

Mechanised Separation Algebra

Gerwin Klein and others (2012) · Springer Berlin Heidelberg

Separation Algebra

Gerwin Klein and others (2012) · Archive of Formal Proofs

seL4 Enforces Integrity

Thomas Sewell and others (2011) · Springer Berlin Heidelberg

seL4: Formal Verification of an Operating-System Kernel

Gerwin Klein and others (2010) · Association for Computing Machinery (ACM)

Experience report: sel4 — formally verifying a high-performance microkernel

Gerwin Klein and others (2009) · Proc. 2009 ACM SIGPLAN International Conference on Functional Programming (ICFP)

Operating system verification—An overview

Gerwin Klein (2009) · Sadhana · Springer Science+Business Media

seL4: Formal Verification of an OS Kernel

Gerwin Klein and others (2009) · Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles · Association for Computing Machinery

Types, Maps and Separation Logic

Rafal Kolanski and others (2009) · Theorem Proving in Higher Order Logics · Springer Berlin Heidelberg

Secure Microkernels, State Monads and Scalable Refinement

David Cock and others (2008) · Springer Berlin Heidelberg

Verified Protection Model of the seL4 Microkernel

Dhammika Elkaduwe and others (2008) · Lecture notes in computer science · Springer Science+Business Media

Mapped Separation Logic

Rafal Kolanski and others (2008) · Springer Berlin Heidelberg

Towards a practical, verified kernel

Kevin Elphinstone and others (2007) · Proceedings of the 11th Workshop on Hot Topics in Operating Systems

Types, bytes, and separation logic

Harvey Tuch and others (2007) · 34th ACM Symposium on Principles of Programming Languages (POPL)

Running the manual: an approach to high-assurance microkernel development

Philip Derrin and others (2006)

A machine-checked model for a Java-like language, virtual machine, and compiler

Gerwin Klein and others (2006) · ACM Transactions on Programming Languages and Systems · Association for Computing Machinery

OS verification — now!

Harvey Tuch and others (2005) · Proceedings of the 10th Workshop on Hot Topics in Operating Systems