• Research

    My work designs a logic framework for reasoning about shared mutable data structures in sequential object-oriented programs. The framework merges read and write efects into the logic along with separation, and provides partial reasoning and global reasoning. A formal connection between supported separation logic and fine-grined region logic can be established in this framework.

    I am intent to graduate in 2017, and interested in research related postions, including internship and Post-doc position.

  • Paper
    • 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