Gerwin Klein - RankMe

103 papers A* 8A 7B 17C 4Journal 34Unranked 22

Year	Rank	Type	Title / Venue / Authors
2025	C	`conf`	A Rely-Guarantee-Based Simulation for Cooperative Semantics. ICTAC Kevin Tran, Johannes Åman Pohjola, Robert Sison, Gerwin Klein
2024	J	`jnl`	AutoCorres2. Arch. Formal Proofs Matthew Brecknell, David Greenaway, Johannes Hölzl, Fabian Immler, Gerwin Klein, Rafal Kolanski, Japheth Lim, Michael Norrish, Norbert Schirmer, Salomon Sickert, Thomas Sewell, Harvey Tuch, Simon Wimmer
2023	B	`conf`	Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems. FM Robert Sison, Scott Buckley, Toby Murray, Gerwin Klein, Gernot Heiser
2023	J	`jnl`	Proving the Absence of Microarchitectural Timing Channels. CoRR Scott Buckley, Robert Sison, Nils Wistoff, Curtis Millar, Toby Murray, Gerwin Klein, Gernot Heiser
2022	J	`jnl`	Cyberassured Systems Engineering at Scale. IEEE Secur. Priv. Darren D. Cofer, Isaac Amundson, Junaid Babar, David S. Hardin, Konrad Slind, Perry Alexander, John Hatcliff, Robby, Gerwin Klein, Corey Lewis, Eric Mercer, John Shackleton
2022	B	`conf`	Property-Based Testing: Climbing the Stairway to Verification. SLE Zilin Chen, Christine Rizkallah, Liam O'Connor, Partha Susarla, Gerwin Klein, Gernot Heiser, Gabriele Keller
2021	J	`jnl`	Cogent: uniqueness types and certifying compilation. J. Funct. Program. Liam O'Connor, Zilin Chen, Christine Rizkallah, Vincent Jackson, Sidney Amani, Gerwin Klein, Toby Murray, Thomas Sewell, Gabriele Keller
2020	J	`jnl`	Formal Reasoning Under Cached Address Translation. J. Autom. Reason. Hira Taqdees Syeda, Gerwin Klein
2020	J	`jnl`	Towards Provable Timing-Channel Prevention. ACM SIGOPS Oper. Syst. Rev. Gernot Heiser, Toby Murray, Gerwin Klein
2020	J	`jnl`	seL4 in Australia: from research to real-world trustworthy systems. Commun. ACM Gernot Heiser, Gerwin Klein, June Andronick
2019	A	`conf`	Can We Prove Time Protection? HotOS Gernot Heiser, Gerwin Klein, Toby C. Murray
2019	J	`jnl`	Can We Prove Time Protection? CoRR Gernot Heiser, Gerwin Klein, Toby C. Murray
2018	J	`jnl`	A Formal Approach to Constructing Secure Air Vehicle Software. Computer Darren D. Cofer, Andrew Gacek, John Backes, Michael W. Whalen, Lee Pike, Adam Foltzer, Michal Podhradsky, Gerwin Klein, Ihor Kuz, June Andronick, Gernot Heiser, Douglas Stuart
2018	B	`conf`	Backwards and Forwards with Separation Logic. ITP Callum Bannister, Peter Höfner, Gerwin Klein
2018	—	`conf`	Bringing Effortless Refinement of Data Layouts to Cogent. ISoLA (1) Liam O'Connor, Zilin Chen, Partha Susarla, Christine Rizkallah, Gerwin Klein, Gabriele Keller
2018	J	`jnl`	Formally verified software in the real world. Commun. ACM Gerwin Klein, June Andronick, Matthew Fernandez, Ihor Kuz, Toby C. Murray, Gernot Heiser
2018	J	`jnl`	Introduction to Milestones in Interactive Theorem Proving. J. Autom. Reason. Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence C. Paulson, Andrei Popescu, Gregor Snelting
2018	B	`conf`	Program Verification in the Presence of Cached Address Translation. ITP Hira Taqdees Syeda, Gerwin Klein
2017	B	`conf`	Reasoning about Translation Lookaside Buffers. LPAR Hira Taqdees Syeda, Gerwin Klein
2017	—	`conf`	The Cogent Case for Property-Based Testing. PLOS@SOSP Zilin Chen, Liam O'Connor, Gabriele Keller, Gerwin Klein, Gernot Heiser
2016	B	`conf`	A Framework for the Automatic Formal Verification of Refinement from Cogent to C. ITP Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby C. Murray, Gabriele Keller, Gerwin Klein
2016	J	`jnl`	COGENT: Certified Compilation for a Functional Systems Language. CoRR Liam O'Connor, Christine Rizkallah, Zilin Chen, Sidney Amani, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Alex Hixon, Gabriele Keller, Toby C. Murray, Gerwin Klein
2016	A*	`conf`	CoGENT: Verifying High-Assurance File System Implementations. ASPLOS Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O'Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby C. Murray, Gerwin Klein, Gernot Heiser
2016	J	`jnl`	Finite Machine Word Library. Arch. Formal Proofs Joel Beeren, Matthew Fernandez, Xin Gao, Gerwin Klein, Rafal Kolanski, Japheth Lim, Corey Lewis, Daniel Matichuk, Thomas Sewell
2016	J	`jnl`	Interactive Theorem Proving - Preface of the Special Issue. J. Autom. Reason. Gerwin Klein, Ruben Gamboa
2016	A	`conf`	Refinement through restraint: bringing down the cost of verification. ICFP Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby C. Murray, Yutaka Nagashima, Thomas Sewell, Gerwin Klein
2015	J	`jnl`	An empirical research agenda for understanding formal methods productivity. Inf. Softw. Technol. D. Ross Jeffery, Mark Staples, June Andronick, Gerwin Klein, Toby C. Murray
2015	B	`conf`	Automated Verification of RPC Stub Code. FM Matthew Fernandez, June Andronick, Gerwin Klein, Ihor Kuz
2015	—	`conf`	Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification. ICSE (1) Daniel Matichuk, Toby C. Murray, June Andronick, D. Ross Jeffery, Gerwin Klein, Mark Staples
2015	J	`jnl`	Qualification of Formal Methods Tools (Dagstuhl Seminar 15182). Dagstuhl Reports Darren D. Cofer, Gerwin Klein, Konrad Slind, Virginie Wiels
2014	—	`ch.`	Applications of Interactive Proof to Data Flow Analysis and Security. Software Systems Safety Gerwin Klein, Tobias Nipkow
2014	J	`jnl`	Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. Gerwin Klein, June Andronick, Kevin Elphinstone, Toby C. Murray, Thomas Sewell, Rafal Kolanski, Gernot Heiser
2014	J	`jnl`	Concerned with the unprivileged: user programs in kernel refinement. Formal Aspects Comput. Matthias Daum, Nelson Billing, Gerwin Klein
2014	—	`book`	Concrete Semantics - With Isabelle/HOL Tobias Nipkow, Gerwin Klein
2014	A*	`conf`	Don't sweat the small stuff: formal verification of C code without the pain. PLDI David Greenaway, Japheth Lim, June Andronick, Gerwin Klein
2014	J	`jnl`	File systems deserve verification too! ACM SIGOPS Oper. Syst. Rev. Gabriele Keller, Toby C. Murray, Sidney Amani, Liam O'Connor, Zilin Chen, Leonid Ryzhyk, Gerwin Klein, Gernot Heiser
2014	B	`ed.`	Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings ITP Gerwin Klein, Ruben Gamboa
2014	A	`conf`	Productivity for proof engineering. ESEM Mark Staples, D. Ross Jeffery, June Andronick, Toby C. Murray, Gerwin Klein, Rafal Kolanski
2014	B	`conf`	Proof Engineering Considered Essential. FM Gerwin Klein
2013	—	`conf`	File systems deserve verification too! PLOS@SOSP Gabriele Keller, Toby C. Murray, Sidney Amani, Liam O'Connor, Zilin Chen, Leonid Ryzhyk, Gerwin Klein, Gernot Heiser
2013	A*	`conf`	Formal specifications better than function points for code sizing. ICSE Mark Staples, Rafal Kolanski, Gerwin Klein, Corey Lewis, June Andronick, Toby C. Murray, D. Ross Jeffery, Len Bass
2013	C	`conf`	Formally Verified System Initialisation. ICFEM Andrew Boyton, June Andronick, Callum Bannister, Matthew Fernandez, Xin Gao, David Greenaway, Gerwin Klein, Corey Lewis, Thomas Sewell
2013	—	`conf`	Towards a verified component platform. PLOS@SOSP Matthew Fernandez, Ihor Kuz, Gerwin Klein, June Andronick
2013	A*	`conf`	Translation validation for a verified OS kernel. PLDI Thomas Arthur Leck Sewell, Magnus O. Myreen, Gerwin Klein
2013	A*	`conf`	seL4: From General Purpose to a Proof of Information Flow Enforcement. IEEE Symposium on Security and Privacy Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, Gerwin Klein
2012	J	`jnl`	AI@NICTA. AI Mag. Nick Barnes, Peter Baumgartner, Tibério S. Caetano, Hugh F. Durrant-Whyte, Gerwin Klein, Penelope Sanderson, Abdul Sattar, Peter J. Stuckey, Sylvie Thiébaux, Pascal Van Hentenryck, Toby Walsh
2012	B	`conf`	Bridging the Gap: Automatic Verified Abstraction of C. ITP David Greenaway, June Andronick, Gerwin Klein
2012	—	`conf`	Challenges and Experiences in Managing Large-Scale Proofs. AISC/MKM/Calculemus Timothy Bourke, Matthias Daum, Gerwin Klein, Rafal Kolanski
2012	—	`ch.`	Interactive Proof: Applications to Semantics. Software Safety and Security Gerwin Klein
2012	J	`jnl`	It's Time for Trustworthy Systems. IEEE Secur. Priv. Gernot Heiser, Toby C. Murray, Gerwin Klein
2012	A*	`conf`	Large-scale formal verification in practice: A process perspective. ICSE June Andronick, D. Ross Jeffery, Gerwin Klein, Rafal Kolanski, Mark Staples, He Zhang, Liming Zhu
2012	B	`conf`	Mechanised Separation Algebra. ITP Gerwin Klein, Rafal Kolanski, Andrew Boyton
2012	B	`conf`	Noninterference for Operating System Kernels. CPP Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Gerwin Klein
2012	—	`ed.`	Proceedings Seventh Conference on Systems Software Verification, SSV 2012, Sydney, Australia, 28-30 November 2012. SSV Franck Cassez, Ralf Huuck, Gerwin Klein, Bastian Schlich
2012	J	`jnl`	Separation Algebra. Arch. Formal Proofs Gerwin Klein, Rafal Kolanski, Andrew Boyton
2012	B	`conf`	Simulation modeling of a large-scale formal verification process. ICSSP He Zhang, Gerwin Klein, Mark Staples, June Andronick, Liming Zhu, Rafal Kolanski
2011	A	`conf`	Provable Security: How Feasible Is It? HotOS Gerwin Klein, Toby C. Murray, Peter Gammie, Thomas Sewell, Simon Winwood
2011	B	`conf`	seL4 Enforces Integrity. ITP Thomas Sewell, Simon Winwood, Peter Gammie, Toby C. Murray, June Andronick, Gerwin Klein
2010	—	`ed.`	5th International Workshop on Systems Software Verification, SSV'10, Vancouver, BC, Canada, October 6-7, 2010 SSV Ralf Huuck, Gerwin Klein, Bastian Schlich
2010	B	`conf`	A Formally Verified OS Kernel. Now What? ITP Gerwin Klein
2010	B	`conf`	From a Verified Kernel towards Verified Systems. APLAS Gerwin Klein
2010	—	`ch.`	Refinement in the Formal Verification of the seL4 Microkernel. Design and Verification of Microprocessor Systems for High-Assurance Applications Gerwin Klein, Thomas Sewell, Simon Winwood
2010	—	`conf`	The L4.verified Project - Next Steps. VSTTE Gerwin Klein
2010	—	`conf`	The road to trustworthy systems. STC@CCS Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz, Leonid Ryzhyk
2010	—	`conf`	capDL: a language for describing capability-based systems. ApSys Ihor Kuz, Gerwin Klein, Corey Lewis, Adam Walker
2010	J	`jnl`	seL4: formal verification of an operating-system kernel. Commun. ACM Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood
2009	J	`jnl`	Correct OS Kernel? Proof? Done! login Usenix Mag. Gerwin Klein
2009	A	`conf`	Experience report: seL4: formally verifying a high-performance microkernel. ICFP Gerwin Klein, Philip Derrin, Kevin Elphinstone
2009	—	`conf`	Mind the Gap. TPHOLs Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David A. Cock, Michael Norrish
2009	J	`jnl`	Operating System Verification. J. Autom. Reason. Gerwin Klein, Ralf Huuck, Bastian Schlich
2009	—	`conf`	Preface. SSV Ralf Huuck, Gerwin Klein, Bastian Schlich
2009	—	`conf`	Types, Maps and Separation Logic. TPHOLs Rafal Kolanski, Gerwin Klein
2009	A*	`conf`	seL4: formal verification of an OS kernel. SOSP Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood
2008	—	`conf`	Mapped Separation Logic. VSTTE Rafal Kolanski, Gerwin Klein
2008	—	`conf`	Preface. SSV Ralf Huuck, Gerwin Klein, Bastian Schlich
2008	—	`ed.`	Proceedings of the 3rd International Workshop on Systems Software Verification, SSV 2008, Sydney, Australia, February 25-27, 2008 SSV Ralf Huuck, Gerwin Klein, Bastian Schlich
2008	—	`ed.`	Proceedings of the 4th International Workshop on Systems Software Verification, SSV 2009, Aachen, Germany, June 22-24, 2009 SSV Ralf Huuck, Gerwin Klein, Bastian Schlich
2008	—	`ed.`	Proceedings of the 5th International Verification Workshop in connection with IJCAR 2008, Sydney, Australia, August 10-11, 2008 VERIFY Bernhard Beckert, Gerwin Klein
2008	—	`conf`	Secure Microkernels, State Monads and Scalable Refinement. TPHOLs David A. Cock, Gerwin Klein, Thomas Sewell
2008	—	`conf`	Title, Preface, Table of Contents. VERIFY Bernhard Beckert, Gerwin Klein
2008	—	`conf`	Verified Protection Model of the seL4 Microkernel. VSTTE Dhammika Elkaduwe, Gerwin Klein, Kevin Elphinstone
2007	—	`conf`	A Termination Checker for Isabelle Hoare Logic. VERIFY Jia Meng, Lawrence C. Paulson, Gerwin Klein
2007	A	`conf`	Towards a Practical, Verified Kernel. HotOS Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe, Gernot Heiser
2007	J	`jnl`	Towards trustworthy computing systems: taking microkernels to the next level. ACM SIGOPS Oper. Syst. Rev. Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein, Stefan M. Petters
2007	A*	`conf`	Types, bytes, and separation logic. POPL Harvey Tuch, Gerwin Klein, Michael Norrish
2006	J	`jnl`	A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Trans. Program. Lang. Syst. Gerwin Klein, Tobias Nipkow
2006	—	`conf`	Formalising the L4 microkernel API. CATS Rafal Kolanski, Gerwin Klein
2006	C	`conf`	On the Automated Synthesis of Proof-Carrying Temporal Reference Monitors. LOPSTR Simon Winwood, Gerwin Klein, Manuel M. T. Chakravarty
2006	C	`conf`	Running the manual: an approach to high-assurance microkernel development. Haskell Philip Derrin, Kevin Elphinstone, Gerwin Klein, David A. Cock, Manuel M. T. Chakravarty
2005	B	`conf`	A Unified Memory Model for Pointers. LPAR Harvey Tuch, Gerwin Klein
2005	J	`jnl`	Jinja is not Java. Arch. Formal Proofs Gerwin Klein, Tobias Nipkow
2005	A	`conf`	OS Verification - Now! HotOS Harvey Tuch, Gerwin Klein, Gernot Heiser
2005	J	`jnl`	Verified Java Bytecode Verification (Verified Java Bytecode Verification). it Inf. Technol. Gerwin Klein
2004	J	`jnl`	Example Submission. Arch. Formal Proofs Gerwin Klein
2004	—	`conf`	Prototyping Proof Carrying Code. IFIP TCS Martin Wildmoser, Tobias Nipkow, Gerwin Klein, Sebastian Nanz
2004	J	`jnl`	Verified bytecode verification and type-certifying compilation. J. Log. Algebraic Methods Program. Gerwin Klein, Martin Strecker
2003	—	`conf`	Verified Bytecode Subroutines. TPHOLs Gerwin Klein, Martin Wildmoser
2003	J	`jnl`	Verified Bytecode Subroutines. J. Autom. Reason. Gerwin Klein, Martin Wildmoser
2003	—	`ch.`	Verified Java Bytecode Verification. Ausgezeichnete Informatikdissertationen Gerwin Klein
2003	—	`—`	Verified Java bytecode verification. Gerwin Klein
2003	J	`jnl`	Verified bytecode verifiers. Theor. Comput. Sci. Gerwin Klein, Tobias Nipkow
2001	J	`jnl`	Verified lightweight bytecode verification. Concurr. Comput. Pract. Exp. Gerwin Klein, Tobias Nipkow
1999	—	`conf`	FormGen: A Generator for Adaptive Forms Based on EasyGUI. HCI (1) Alfons Brandl, Gerwin Klein