Corey Lewis
Visiting Fellow; Engineer at Proofcraft
Research Interests
Corey was a senior proof engineer and the lead engineer for verifying multi-core seL4. During his time at TS he has been involved in a wide variety of projects to do with seL4. These include developing the original CapDL translation tools, helping complete the information flow proofs, and contributing to the verification of the seL4 MCS extensions. His research interests include formal methods, functional programming, and program verification. Corey now works at Proofcraft.
Contact Details
| Phone: | +61 2 9490 5858 |
|---|---|
| Email: | corey.lewis@unsw.edu.au |
More contact information is available at the Contact page.
Projects
Past |
Qualifications
Bachelor of Science (Advanced Mathematics), University of New South Wales
Publications
Best Papers
 
|
 |
Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein seL4: From general purpose to a proof of information flow enforcement IEEE Symposium on Security and Privacy, pp. 415–429, San Francisco, CA, May, 2013 |
Trustworthy Systems Group Papers
2017
|
|
|
Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah and Joey Tuong COMPLX: A verification framework for concurrent imperative programs International Conference on Certified Programs and Proofs, pp. 138–150, Paris, France, January, 2017 |
2016
|
|
|
June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan and Christine Rizkallah Proof of OS scheduling behavior in the presence of interrupt-induced concurrency International Conference on Interactive Theorem Proving, pp. 52–68, Nancy, France, August, 2016 |
2015
|
|
|
June Andronick, Corey Lewis and Carroll Morgan Controlled Owicki-Gries concurrency: reasoning about the preemptible eChronos embedded operating system Workshop on Models for Formal Analysis of Real Systems (MARS 2015), pp. 10–24, Suva, Fiji, November, 2015 |
2013
|
|
|
Andrew Boyton, June Andronick, Callum Bannister, Matthew Fernandez, Xin Gao, David Greenaway, Gerwin Klein, Corey Lewis and Thomas Sewell Formally verified system initialisation International Conference on Formal Engineering Methods, pp. 70–85, Queenstown, New Zealand, October, 2013 |
|
|
|
Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein seL4: From general purpose to a proof of information flow enforcement IEEE Symposium on Security and Privacy, pp. 415–429, San Francisco, CA, May, 2013 |
|
|
|
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 |
2010
|
|
|
Ihor Kuz, Gerwin Klein, Corey Lewis and Adam Christopher Walker capDL: A language for describing capability-based systems Asia-Pacific Workshop on Systems (APSys), pp. 31–35, New Delhi, India, August, 2010 |