Lecturer
My research interests, in large scale, focus on logics and their related theories in computer science, encompassing dynamic logics, relational calculi, temporal logics, process algebras, etc. Particularly, I am interested in their applications for system/program specifications and verifications.
Currently, our research work includes the following aspects: Dynamic logics and deduction-based verification , where we develop verification methods and techniques for synchronous models of reactive systems using dynamic logics; Formal specification languages for Real-time Embedded Systems, where we create high-level formal specification languages and associated verification techniques to handle logical time constraints and properties of real-time embedded systems and system models; Proof theories of regular expressions, where we investigate proof theories of regular expression equations with respect to bisimulation equivalences.
