|
John Hopcroft Center for Computer Science Shanghai Jiao Tong University Room 201, IEEE Building No.1, No.800 Dongchuan Road, Minhang District Shanghai 200240, China Email: <first name>.<last name> at sjtu.edu.cn |
I am currently a Tenure-Track Associate Professor at Shanghai Jiao Tong University. Before that, I was a postdoctoral researcher at Yale University supervised by Zhong Shao from December 2016 to December 2019. I obtained my Ph.D. degree at the University of Minnesota, Twin Cities under the advisory of Gopalan Nadathur. More detailed information can be found in my curriculum vitae.
I am broadly interested in the following research areas:
My current research focuses on techniques and frameworks for verifying system software (including compilers and operating systems). I am also involved in developing theories and frameworks for programming, specifying and verifying rule-based relational specifications. This line of research centers on the development of the Abella theorem prover.
I am always looking for self-motivated undergraduate, master and Ph.D. students to collaborate with. If you are interested in or around my research areas, feel free to contact me.
A major focus of my research is to develop software (and prototypes) to testify the strength of my research ideas in practice. The following is a list of software and frameworks I have led or participated in developing. Their detailed descriptions could be found in my CV.
A verified C compiler that generates machine code base on CompCert.
A lightweight generalization of CompCert to supports modular reasoning about local memory (e.g., local stacks of threads).
A verified compiler supporting end-to-end and separate compilation of heterogeneous programs (i.e., modules written in different programming languages) without exposing compiler implementation details.
An extension of CompCertO to support multi-threaded programs with sharing of stack-allocated data.
A verified compiler front-end of CompCert targeting a subset of the Rust programming language.
My research group made notable contributions to Charon and Eurydice to build a production level compilation chain from Rust to C.
A framework for verifying concurrent programs organized as layers of isolated objects.
A framework for specifying and automatically generating verified machine instruction encoders and decoders (e.g. for X86 and RISC-V).
A framework for generically reasoning about programming languages with binding structures based on Locally Nameless Representation. Yicheng Ni used it to find and fix an error in the proof of compactness for PCF in Bob Harper's book "Practical Foundations for Programming Languages". This fix has been incorporated into the book's errata.
An interactive theorem-prover noteworthy for its support of higher-order abstract syntax and for the two-level logic approach to reasoning about formal specifications.
(Corresponding authors are marked with *)
https://orcid.org/0000-0003-3990-2418