Rafal Kolanski

17 papers A* 3A 1B 2Journal 5Unranked 5
YearRankTypeTitle / Venue / Authors
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
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
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 A conf
Productivity for proof engineering.
ESEM
Mark Staples, D. Ross Jeffery, June Andronick, Toby C. Murray, Gerwin Klein, Rafal Kolanski
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
2012 — conf
Challenges and Experiences in Managing Large-Scale Proofs.
AISC/MKM/Calculemus
Timothy Bourke, Matthias Daum, Gerwin Klein, Rafal Kolanski
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 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 — —
Verification of programs in virtual memory using separation logic.
Rafal Kolanski
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 — 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
A Logic for Virtual Memory.
SSV
Rafal Kolanski
2008 — conf
Mapped Separation Logic.
VSTTE
Rafal Kolanski, Gerwin Klein
2006 — conf
Formalising the L4 microkernel API.
CATS
Rafal Kolanski, Gerwin Klein