Software engineer · Formal verification
Joe Hattori
I am a software engineer at Google with research interests in formal verification for systems software.
I am interested in using proof assistants to build machine-checked arguments about real systems, and in combining interactive theorem proving with automated techniques for production-scale, low-level code.
01
Research
My primary interests are theorem proving and formal verification, especially their application to systems software. I am particularly interested in interactive theorem proving for reasoning about concurrency, ownership, and low-level interfaces.
My previous work uses automated program analysis to find resource-management bugs in Linux kernel drivers. More broadly, I am interested in proof assistants, program logics, operating systems, programming languages, and making machine-checked verification useful for code that runs in the real world.
02
Publications
CAV 2026
Distinguished Paper Award
Automatic Detection of Reference Counting Bugs in Linux Kernel Drivers
Joe Hattori, Naoki Kobayashi, and Ken Sakayori.
38th International Conference on Computer Aided Verification (CAV), 2026.
DrvHorn reduces Linux-driver reference-count verification to assertion checking. Applied to all platform drivers in Linux v6.6, it found 545 bugs, including 424 previously unknown bugs; 47 resulting patches were merged into the Linux kernel.
SoCC 2023
Parrotfish: Parametric Regression for Optimizing Serverless Functions
Arshia Moghimi, Joe Hattori, Alexander Li, Mehdi Ben Chikha, and Mohammad Shahrad.
ACM Symposium on Cloud Computing (SoCC), 2023.
USENIX ATC 2023
UnFaaSener: Latency and Cost Aware Offloading of Functions from Serverless Platforms
Ghazal Sadeghian, Mohamed Elsakhawy, Mohanna Shahrad, Joe Hattori, and Mohammad Shahrad.
2023 USENIX Annual Technical Conference (USENIX ATC), 2023.
WoSC 2022
Sentinel: A Fast and Memory-Efficient Serverless Architecture for Lightweight Applications
Joe Hattori and Shinpei Kato.
8th International Workshop on Serverless Computing (WoSC), 2022.
03
Background
2025–present · Software Engineer
-
Working on Android/Googlebook performance.
-
Contributing to Kraken, a tool for verifying sequential assembly code, with a focus on separation logic and proof automation in Lean4, including a contribution merged into Lean4’s standard library.
-
crosvm-verif: Verifying selected critical components of crosvm, a secure, high-performance virtual machine monitor used in Android, ChromeOS, and Googlebook, by translating Rust code to Lean4 using Aeneas and proving functional correctness properties. Discovered and fixed three bugs.
-
IrisLKMM: Formalized a fragment of the Linux Kernel Memory Model in Rocq, connected it to an operational semantics and an Iris program logic, and proved operational soundness, completeness, and Iris adequacy for completed executions.
The University of Tokyo
2018–2025
Bachelor’s and Master’s degrees in Computer Science · advised by Prof. Naoki Kobayashi