Rafal Kolanski - Graduate Researcher/Part-time Research Engineer
Trustworthy Embedded Systems Project
Research Interests
Rafal is interested in the verification of system-level software, particularly software involving virtual memory such as operating systems. He is very interested in separation logic and the possibilities it creates for making this verification task easier.
NICTA Projects
L4 pilot project
L4.verified
Career Summary
Research Assistant on the L4 pilot project (precursor to L4.verified) in 2005.
Qualifications
Bachelor of Engineering in Software Engineering, University of New South Wales, 2004
Contact Details
| Email: | rafalk@cse.unsw.edu.au |
|---|---|
| Web: | http://www.cse.unsw.edu.au/~rafalk |
More contact information is available at the ERTOS Contacts page.
Publications
Best Papers
|
 |
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 OS kernel Communications of the ACM, 53(6), 107–115, (June, 2010) |
|
|
|
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 Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, October, 2009 Best Paper Award! |
NICTA Papers
2010
|
|
|
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 OS kernel Communications of the ACM, 53(6), 107–115, (June, 2010) |
2009
|
|
|
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 Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, October, 2009 Best Paper Award! |
|
|
|
Rafal Kolanski and Gerwin Klein Types, maps and separation logic Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, Munich, Germany, August, 2009 |
2008
|
|
|
Rafal Kolanski and Gerwin Klein Mapped separation logic Proceedings of Verified Software: Theories, Tools and Experiments 2008, Toronto, Canada, October, 2008 |
|
|
|
Rafal Kolanski A logic for virtual memory Proceedings of the 3rd Workshop on Systems Software Verification, Sydney, Australia, February, 2008 |
2006
|
|
|
Kevin Elphinstone, Gerwin Klein and Rafal Kolanski Formalising a high-performance microkernel Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06), Seattle, USA, August, 2006 |
|
|
|
Rafal Kolanski and Gerwin Klein Formalising the L4 microkernel API Computing: The Australasian Theory Symposium (CATS 06), Hobart, Australia, January, 2006 |
2005
|
|
|
Rafal Kolanski A formal model of the L4 micro-kernel API using the B method Technical Report Technical Report 05-00029-1, National ICT Australia, 2005 |