Yuyan Bao

Yuyan Bao

Research

My main research interests are centered around Programming Languages and Software Engineering, with a focus on formal methods and reasoning about the correctness of programs. With the increasing prevalence of applications for software, we are also witnessing a growth in the number of programming languages themselves, e.g., domain-specific languages.

As they are specialized to a particular application domain, e.g., mobile applications, distributed systems,cryptographic protocols, etc., the constant challenge has been to reason about the correctness of the generated programs using a uniform framework. My interests and the goal of my research have always been to investigate the structure and semantics of programming languages and to come up with methods and methodologies to reason about their correctness. A long term goal is to transition research tools and methodologies into practice.

The results of my research include theoretical foundations for reasoning about object-oriented programs and higher-order functional programs with mutable state, and designing frameworks and building automated deductive verification tools for analyzing programs that compute with sensitive information.

Collaborations

With Arie Gurfinkel and Werner Dietl at Waterloo, I am working on detecting Java Cryptographic APIs misuses.

With Tiark Rompf at Purdue, I am working on Reachability Types and Dependency Tracking for higher-order functional programming languages with mutable states.

Projects