Skip to main content

Rafal Kolanski

Rafal Kolanski
Senior Research Engineer

Research Interests

Rafal is interested in the formal verification of high assurance, system-level software, both from the perspective of verification in practice, but also proof maintenance and increasing the proof coverage of already verified systems.

Contact Details

Phone: +61 2 9490 5864
Email:Rafal.Kolanski@data61.csiro.au

More contact information is available at the Contact page.

Photo of Rafal Kolanski

Projects

Current

Past

Qualifications

Bachelor of Engineering in Software Engineering, University of New South Wales, 2004.

Ph.D. from the University of New South Wales, at the Computer Science and Engineering faculty, 2011.

NICTA Papers

2014

Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser
Comprehensive formal verification of an OS microkernel
ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014

2013

Abstract PDF Mark Staples, Rafal Kolanski, Gerwin Klein, Corey Lewis, June Andronick, Toby Murray, Ross Jeffery and Len Bass
Formal specifications better than function points for code sizing
International Conference on Software Engineering, pp. 1257-1260, San Francisco, USA, May, 2013

2012

Abstract PDF Gerwin Klein, Rafal Kolanski and Andrew Boyton
Mechanised separation algebra
International Conference on Interactive Theorem Proving, pp. 332-337, Princeton, USA, August, 2012
Abstract PDF Timothy Bourke, Matthias Daum, Gerwin Klein and Rafal Kolanski
Challenges and experiences in managing large-scale proofs
Conferences on Intelligent Computer Mathematics (CICM) / Mathematical Knowledge Management, pp. 32-48, Bremen, Germany, July, 2012
Abstract PDF June Andronick, Ross Jeffery, Gerwin Klein, Rafal Kolanski, Mark Staples, Jason Zhang and Liming Zhu
Large-scale formal verification in practice: A process perspective
International Conference on Software Engineering, pp. 1002-1011, Zurich, Switzerland, June, 2012
Abstract PDF Jason Zhang, Gerwin Klein, Mark Staples, June Andronick, Liming Zhu and Rafal Kolanski
Simulation modeling of a large scale formal verification process
International Conference on Software and Systems Process, pp. 3-12, Zurich, Switzerland, June, 2012

2011

Abstract PDF Rafal Kolanski
Verification of programs in virtual memory using separation logic
PhD Thesis, UNSW, Sydney, Australia, July, 2011

2010

Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood
seL4: Formal verification of an operating-system kernel
Communications of the ACM, Volume 53, Number 6, pp. 107-115, June, 2010
Research Highlights paper

2009

Abstract
Slides
PDF
Presentation Video
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood
seL4: Formal verification of an OS kernel
ACM Symposium on Operating Systems Principles, pp. 207-220, Big Sky, MT, USA, October, 2009
Abstract PDF Rafal Kolanski and Gerwin Klein
Types, maps and separation logic
International Conference on Theorem Proving in Higher Order Logics, pp. 276-292, Munich, Germany, August, 2009

2008

Abstract PDF Rafal Kolanski and Gerwin Klein
Mapped separation logic
Verified Software: Theories, Tools and Experiments, pp. 15-29, Toronto, Canada, October, 2008
Abstract PDF Rafal Kolanski
A logic for virtual memory
Systems Software Verification, pp. 61-77, Sydney, Australia, July, 2008

2006

Abstract PDF Kevin Elphinstone, Gerwin Klein and Rafal Kolanski
Formalising a high-performance microkernel
Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06), pp. 1-7, Seattle, USA, August, 2006
Abstract PDF Gerwin Klein and Rafal Kolanski
Formalising the L4 microkernel API
Computing: The Australasian Theory Symposium (CATS), pp. 53–68, Hobart, Australia, January, 2006

2005

Abstract PDF Rafal Kolanski
A formal model of the L4 micro-kernel API using the B method
Technical Report Technical Report 05-00029-1, NICTA, 2005