Rafal Kolanski

According to our database, Rafal Kolanski authored at least 17 papers between 2006 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

AutoCorres2.

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

Arch. Formal Proofs, 2024

2016

Finite Machine Word Library.

Joel Beeren, Matthew Fernandez, Xin Gao, Gerwin Klein, Rafal Kolanski, Japheth Lim, Corey Lewis, Daniel Matichuk, Thomas Sewell

Arch. Formal Proofs, 2016

2014

Comprehensive formal verification of an OS microkernel.

Gerwin Klein, June Andronick, Kevin Elphinstone, Toby C. Murray, Thomas Sewell, Rafal Kolanski, Gernot Heiser

ACM Trans. Comput. Syst., 2014

Productivity for proof engineering.

Mark Staples, D. Ross Jeffery, June Andronick, Toby C. Murray, Gerwin Klein, Rafal Kolanski

Proceedings of the 2014 ACM-IEEE International Symposium on Empirical Software Engineering and Measurement, 2014

2013

Formal specifications better than function points for code sizing.

Mark Staples, Rafal Kolanski, Gerwin Klein, Corey Lewis, June Andronick, Toby C. Murray, D. Ross Jeffery, Len Bass

Proceedings of the 35th International Conference on Software Engineering, 2013

2012

Separation Algebra.

Gerwin Klein, Rafal Kolanski, Andrew Boyton

Arch. Formal Proofs, 2012

Mechanised Separation Algebra.

Gerwin Klein, Rafal Kolanski, Andrew Boyton

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Simulation modeling of a large-scale formal verification process.

He Zhang, Gerwin Klein, Mark Staples, June Andronick, Liming Zhu, Rafal Kolanski

Proceedings of the 2012 International Conference on Software and System Process, 2012

Large-scale formal verification in practice: A process perspective.

June Andronick, D. Ross Jeffery, Gerwin Klein, Rafal Kolanski, Mark Staples, He Zhang, Liming Zhu

Proceedings of the 34th International Conference on Software Engineering, 2012

Challenges and Experiences in Managing Large-Scale Proofs.

Timothy Bourke, Matthias Daum, Gerwin Klein, Rafal Kolanski

Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2012

2011

Verification of programs in virtual memory using separation logic.

Rafal Kolanski

PhD thesis, 2011

2010

seL4: formal verification of an operating-system kernel.

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

Commun. ACM, 2010

2009

Types, Maps and Separation Logic.

Rafal Kolanski, Gerwin Klein

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

seL4: formal verification of an OS kernel.

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

Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, 2009

2008

A Logic for Virtual Memory.

Rafal Kolanski

Proceedings of the 3rd International Workshop on Systems Software Verification, 2008

Mapped Separation Logic.

Rafal Kolanski, Gerwin Klein

Proceedings of the Verified Software: Theories, 2008

2006

Formalising the L4 microkernel API.

Rafal Kolanski, Gerwin Klein

Proceedings of the Theory of Computing 2006, 2006