Gerwin Klein
6 references under this name, matched as it is written. Somebody else may write under it too, and the same person may appear here spelled another way.
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
The seL4 project told from several distances: the machine-checked proof of functional correctness for an operating-system kernel, with the groundwork in a machine-checked model for a Java-like language and in types, bytes and separation logic -- reasoning about a kernel means reasoning about bytes rather than an abstract heap. Two retrospectives follow, one arguing that verified software in the real world can be done at all, the other an account of deployment rather than of proof.
seL4 in Australia: From Research to Real-World Trustworthy Systems
Gernot Heiser and others (2020) · Communications of the ACM · Association for Computing Machinery
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
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, bytes, and separation logic
Harvey Tuch and others (2007) · 34th ACM Symposium on Principles of Programming Languages (POPL)
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