Keiichi Watanabe

Keiichi Watanabe

A Software Engineer at Google

About Me

My name is Keiichi Watanabe. I’m a senior software engineer at Google. I earned a Master’s degree in Computer Science from the University of Tokyo in 2018.

Education

  • M.S. in Computer Science, University of Tokyo, 2018
  • B.S. in Information Science, University of Tokyo, 2016

Work Experiences

Software Engineer, Google Japan

April 2018 - Present

A senior software engineer on the ChromeOS platform team. I’m a tech lead for a team that develops virtualization technology to run Android apps on Chromebooks.

  • Developing and maintaining crosvm, a multi-platform virtual machine monitor written in Rust for ChromeOS.
  • Developing and optimizing file systems for Android VM.
  • Designed and implemented a virtio-video decoder to deliver hardware-accelerated video decoding inside Android VM. Proposed patches to the Linux community.

Publications

Peer-reviewed Conference Papers

  • Keiichi Watanabe, Takeshi Tsukada, Hiroki Oshikawa and Naoki Kobayashi: “Reduction from Branching-Time Property Verification of Higher-Order Programs to HFL Validity Checking.” In the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2019), Cascais, Portugal, 2019. PDF
  • Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe: “Higher-Order Program Verification via HFL Model Checking.” In the 27th European Symposium on Programming (ESOP 2018), Thessaloniki, Greece, 2018. arXiv
  • Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada and Naoki Kobayashi: “Automatically Disproving Fair Termination of Higher-Order Functional Programs.” In the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), Nara, Japan, 2016. Paper

Book

  • Akira Kawata, Yuki Koike, Keiichi Watanabe, Takaya Saeki, and Mizuki Arata: “Binary Hacks Rebooted”, O’Reilly Japan, August 2024. Amazon

Software

  • Crosvm - Virtual machine monitor in Rust for ChromeOS
  • Constexpr-8cc - C compiler implemented as C++’s conctexpr
  • Libtracecmd-rs - Rust library for analyzing and profiling Linux’s ftrace data
  • UCC - C89 compiler in OCaml
  • A-Puzzle-A-Day solver - A puzzle solver implemented in Rust + WebAssembly + TypeScript.

For more of my open-source projects, see GitHub.