Scientific Research

    My research area mainly lies in formal methods. I am interested in model checking, temporal logics, separation logic and their applications to program verification and AI planning. More specifically, I propose a spatio-temporal logic, named PPTL^SL, which integrates a decidable fragment of separation logic and PPTL (Propositional Projection Temporal Logic). PPTL^SL is employed to express heap evolution properties of pointer programs and search control knowledge in AI planning. A unified model checking approach and an efficient planning algorithm are also proposed for PPTL^SL. The corresponding work has been published in some top-tier conferences and journals (e.g., IJCAI, TCS and TKDE).