• Research Interests

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

    The long term goal of my research is to develop reliable and dependable software. Currently, much software is developed without precise specification, and thus cannot be verified. To explain further, many methodologies have been proposed for verifying programs either based on research languages, or on a subset of programming languages used in software industry. My research interest is to bridge the gap between research and the software industry. On one hand, I am interested in formalizing programming languages used in the software industry and investigating their semantic models, and understanding how to specify and verify such programs. On the other hand, I am interested in developing new programming languages whose semantic models are a good fit for formal specification and verification, but which do not reduce the productivity of engineers.

    In pursuing this goal, I have been working on local reasoning and modular reasoning about object-oriented programs, which is one of the widely-used programming models in the software industry. I have accomplished two tasks. One is investigating and combining different methodologies for reasoning about the framing properties, which is one of the important problems in modular verification. In particular, I designed UFRL that allows specifications written in the styles of SSL and FRL to be interoperate with each other. The result simplifies specifications and makes reasoning about unrestricted shared mutable data structures easier. The other is defining a frame condition for behavioral subtyping, which is proved sound. Behavioral subtyping is necessary and sufficient for the validity of supertype abstraction, which allows one to modular reasoning about dynamic dispatch.

    I defended in Nov, 2017, and am going to graduate in Dec, 2017. Currently, I am looking for a research related postion, including research internship and Post-doc position.

    Here is my CV.

  • Publications and Technical Reports
    • Yuyan Bao, Gary T. Leavens, and Gidon Ernst. Conditional Effects in Fine-Grained Region Logic. In Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs , FTfJP '15, pages 5:1-5:6, New York, NY, USA, 2015. ACM. [ bib | DOI | http ]
    • Yuyan Bao, Gary T. Leavens, and Gidon Ernst. Technical Report for Conditional Effects in Fine-Grained Region Logic. Dept. of Electrical Engineering and Computer Science, University of Central Florida, CS-TR-15-01, August 2015. [PDF]
    • Yuyan Bao, Gary T. Leavens, and Gidon Ernst. Technical Report for Unifying Separation Logic and Region Logic to Allow Interoperability. Dept. of Electrical Engineering and Computer Science, University of Central Florida, CS-TR-16-01, Dec 2016. [PDF]
  • Projects