Complex systems, such as distributed systems and operating systems, need formal verification to guarantee the correctness. However, formal verification is often considered sophisticated and time-consuming and thus it is not usually applied to most of production code and performance-optimized code that tends to have complex code structures. I'm exploring ways to co-design the system and formal verification so that code verification can be simplified and verified code runs fast.

I am interested in designing, building, and reasoning about distributed systems, such as consensus protocols and systems with different consistency semantics. My current research focuses on the interactions and compositions of multiple distributed systems in a serverless computing context. 

Cloud storage systems can be considered as distributed systems but there are specialized concerns regarding how to store and mutate the data and how the system should interact with lower-level storage devices. More specifically, my research topics include the use of various transactional mechanisms, consistency semantics, and new storage media technologies in the cloud and distributed environment.

New form of applications always need a system support to run efficiently. I'm investigating ways to accelerate and optimize control and data flows of deep neural network from a systems viewpoint.