Short Bio

Email: (

I am a Youngth Research Professor (青年研究员)1 at East China Normal University (ECNU). I got my Ph.D. from ECNU in 2014, advised by Professor Jifeng He and Geguang Pu. Then I went to Rice University (2014.9 - 2017.9) as a postdoc, working with Professor Moshe Y. Vardi. After that, I moved to Iowa State University (ISU) for another two-years’ postdoc, working with Professor Kristin Y. Rozier. Starting from November of 2019, I became a full-time faculty at ECNU.

My current research interests include automatic formal verification, logics and automata theory. I particularly interet in the application of formal methods to the industry, e.g., hardware, railway interlocking system, aerospace and et al. In recent years, I collaborated with colleages from such domains and developed tools (model checkers and constraint solvers) to guarantee the corresponding systems and designs.

The majority of my previous (and in the predictable future) research efforts fall in model checking and LTL (Linear Temporal Logic) reasoning, including LTL-to-automata, LTL satisfiability checking and synthesis/realizibility. Together with collaborators, I proposed CAR (Complementary Approaximate Reachability), a new safety model checking algorithm, and developed aalta/aaltaf, an LTL/LTLf satisfiability checker, which are state-of-the-arts.

  1. The position is similar to the tenured-track associate professor.