Gerwin Klein

Available identifiers

zbMath Open klein.gerwinDBLP74/2171WikidataQ88908200 ScholiaQ88908200MaRDI QIDQ736847

List of research outcomes

Publication	Date of Publication	Type
Cogent: uniqueness types and certifying compilation	2021-12-27	Paper
Formal reasoning under cached address translation	2020-11-02	Paper
Reasoning about Translation Lookaside Buffers	2019-01-10	Paper
Backwards and forwards with separation logic	2018-10-04	Paper
Program verification in the presence of cached address translation	2018-10-04	Paper
Refinement through restraint: bringing down the cost of verification	2017-05-10	Paper
A framework for the automatic formal verification of refinement from \textsc{Cogent} to C	2016-10-27	Paper
Concerned with the unprivileged: user programs in kernel refinement	2016-08-05	Paper
Experience report: seL4, formally verifying a high-performance microkernel	2015-01-06	Paper
Concrete semantics. With Isabelle/HOL	2014-10-23	Paper
Types, bytes, and separation logic	2014-09-12	Paper
Noninterference for operating system kernels	2013-04-19	Paper
Bridging the Gap: Automatic Verified Abstraction of C	2012-09-20	Paper
Mechanised Separation Algebra	2012-09-20	Paper
Challenges and experiences in managing large-scale proofs	2012-09-07	Paper
seL4 enforces integrity	2011-08-17	Paper
Operating system verification---an overview	2009-11-23	Paper
Types, Maps and Separation Logic	2009-10-20	Paper
Secure Microkernels, State Monads and Scalable Refinement	2008-12-04	Paper
A Unified Memory Model for Pointers	2008-05-27	Paper
On the Automated Synthesis of Proof-Carrying Temporal Reference Monitors	2007-09-10	Paper
https://portal.mardi4nfdi.de/entity/Q4673417	2005-04-29	Paper
Verified bytecode verification and type-certifying compilation	2004-10-14	Paper
Verified bytecode subroutines	2003-09-09	Paper
Verified bytecode verifiers.	2003-05-25	Paper
Verified lightweight bytecode verification	2002-05-01	Paper

Research outcomes over time

This page was built for person: Gerwin Klein