Simon is interested in software correctness, in particular formally verified systems and language based security. He is currently working on the l4.verified project.
Simon collaborates with the Programming Languages and Systems group at the University of New South Wales.
In 2002 Simon was awarded a Bachelor of Engineering in Computer Engineering (Hons. 1) by the University of New South Wales. He submitted his PhD Apr. 2010.
|Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein|
seL4 enforces integrity
International Conference on Interactive Theorem Proving, pp. 325-340, Nijmegen, The Netherlands, August, 2011
|Gerwin Klein, Toby Murray, Peter Gammie, Thomas Sewell and Simon Winwood|
Provable security: How feasible is it?
Workshop on Hot Topics in Operating Systems, pp. 5, Napa, USA, May, 2011
|Simon Winwood and Manuel Chakravarty|
Singleton : A general-purpose dependently-typed assembly language
The Sixth ACM SIGPLAN Workshop on Types in Language Design and Implementation, pp. 3–14, Austin, Texas, USA, January, 2011
|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
|Gerwin Klein, Thomas Sewell and Simon Winwood|
Refinement in the formal verification of seL4
Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 323-339, Springer, 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
ACM Symposium on Operating Systems Principles, pp. 207-220, Big Sky, MT, USA, October, 2009
|Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock and Michael Norrish|
Mind the gap: A verification framework for low-level C
International Conference on Theorem Proving in Higher Order Logics, pp. 500-515, Munich, Germany, August, 2009