Gerwin Klein
From MaRDI portal
List of research outcomes
This list is not complete and representing at the moment only items from zbMATH Open and arXiv. We are working on additional sources - please check back here soon!
| Publication | Date of Publication | Type |
|---|---|---|
| Cogent: uniqueness types and certifying compilation Journal of Functional Programming | 2021-12-27 | Paper |
| Formal reasoning under cached address translation Journal of Automated Reasoning | 2020-11-02 | Paper |
| Reasoning about Translation Lookaside Buffers EPiC Series in Computing | 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 Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming | 2017-05-10 | Paper |
| A framework for the automatic formal verification of refinement from \textsc{Cogent} to C Interactive Theorem Proving | 2016-10-27 | Paper |
| Concerned with the unprivileged: user programs in kernel refinement Formal Aspects of Computing | 2016-08-05 | Paper |
| Experience report: seL4, formally verifying a high-performance microkernel Proceedings of the 14th ACM SIGPLAN international conference on Functional programming | 2015-01-06 | Paper |
| Concrete semantics. With Isabelle/HOL | 2014-10-23 | Paper |
| Types, bytes, and separation logic Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-09-12 | Paper |
| Noninterference for operating system kernels Certified Programs and Proofs | 2013-04-19 | Paper |
| Bridging the Gap: Automatic Verified Abstraction of C Interactive Theorem Proving | 2012-09-20 | Paper |
| Mechanised Separation Algebra Interactive Theorem Proving | 2012-09-20 | Paper |
| Challenges and experiences in managing large-scale proofs Lecture Notes in Computer Science | 2012-09-07 | Paper |
| seL4 enforces integrity Interactive Theorem Proving | 2011-08-17 | Paper |
| Operating system verification---an overview Sādhanā | 2009-11-23 | Paper |
| Types, Maps and Separation Logic Lecture Notes in Computer Science | 2009-10-20 | Paper |
| Secure Microkernels, State Monads and Scalable Refinement Lecture Notes in Computer Science | 2008-12-04 | Paper |
| A Unified Memory Model for Pointers Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
| On the Automated Synthesis of Proof-Carrying Temporal Reference Monitors Logic-Based Program Synthesis and Transformation | 2007-09-10 | Paper |
| scientific article; zbMATH DE number 2163030 (Why is no real title available?) | 2005-04-29 | Paper |
| Verified bytecode verification and type-certifying compilation The Journal of Logic and Algebraic Programming | 2004-10-14 | Paper |
| Verified bytecode subroutines Journal of Automated Reasoning | 2003-09-09 | Paper |
| Verified bytecode verifiers. Theoretical Computer Science | 2003-05-25 | Paper |
| Verified lightweight bytecode verification Concurrency and Computation: Practice and Experience | 2002-05-01 | Paper |
Research outcomes over time
This page was built for person: Gerwin Klein
