Formal specification and verification, specification language design and semnatics, programming languages

I conduct research in building safety critical, mission critical and security critical large, and extensible systems. A failure of these systems may result in loss of life, severe damage to enquipment or environments, and loos of business or damage to reputation. Precise system specifications and reliable proofs that the implementation satisfies the specification are necessary.

My work focuses on improving the productivity of writing specifications and building reliable systems though automated static reasoning, as static reasoning does not increase run time overhead. One of the concerns of my work is modularity. Modularity allows us to verify larege, extensible systems compositionally, i.e., a verified system does not need be re-verified when the system is extended.

In pursing this goal, I designed a specification language that helps one to describe and prove programs with shared mutable data structures, and delopved methodologies for statically reasoning about dynamic method calls. Both are important for modularly building reliable extensible systems.

I graduated in Dec, 2017, and am looking for a research related postion, including research internship and Post-doc position.

Here is my CV. Here is my dissertation.