Miki Tanaka
Senior Proof Engineer
Research Interests
Miki is interested in formal verification techniques and their application to software systems, and broadly proof engineering as a discipline. Miki has contributed to the verification of architecture porting for seL4 and also the verification of the seL4 MCS extensions as the technical lead. Miki is currently involved in a project for device driver verification using the Pancake language (based on cakeML/HOL4).
Contact Details
| Email: | Miki.Tanaka@unsw.edu.au |
|---|
More contact information is available at the Contact page.
Projects
Current |
Past |
Publications
Trustworthy Systems Group Papers
2025
 
|
 |
Liam Murphy, Albert Rizaldi, Lesley Rossouw, Chen George, James Treloar, Hammond Pearce, Miki Tanaka and Gernot Heiser High-fidelity specification of real-world devices Workshop on Programming Languages and Operating Systems (PLOS), October, 2025 |
|
|
|
Junming Zhao, Alessandro Legnani, Tiana Tsang Ung, H. Truong, Tsun Wang Sau, Miki Tanaka, Johannes Åman Pohjola, Thomas Sewell, Rob Sison, Hira Syeda, Magnus Myreen, Michael Norrish and Gernot Heiser Verifying device drivers with Pancake arXiv preprint, January, 2025 |
2023
|
|
|
Johannes Åman Pohjola, Hira Taqdees Syeda, Miki Tanaka, Krishnan Winter, Tsun Wang Sau, Benjamin Nott, Tiana Tsang Ung, Craig McLaughlin, Remy Seassau, Magnus O. Myreen, Michael Norrish and Gernot Heiser Pancake: verified systems programming made sweeter Workshop on Programming Languages and Operating Systems (PLOS), Koblenz, DE, October, 2023 |