• 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 Fine-Grained Region Logic and Unified Fine-Grained Region Logic. Dept. of Electrical Engineering and Computer Science, University of Central Florida, CS-TR-16-01, Dec 2016. [PDF]
  • Projects