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
A grouping.
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.
27 references
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