Today, software controls and even defines much of the technology we rely on, but our ability to construct large, complex software systems far outstrips our ability to ensure they are reliable and secure. The result is a plethora of faulty software with defects that range from minor glitches to critical security vulnerabilities.

 The goal of my research is to discover fundamental new ways to improve software reliability and security, by developing program analysis tools and techniques that reason about the behavior of software.  In this talk, I will give an overview of this research area, focusing on three recent projects: (1) Types for Scripting Languages.  In this project, we have been exploring ways to bring the benefits of static typing to Ruby, a popular, object-oriented dynamic language. I will describe a sequence of efforts with this aim, beginning with a purely static approach and ending with a hybrid static-dynamic system that is well-aligned with typical uses of Ruby.  (2) Program Synthesis. In this project, we have been studying the problem of constructing a program semi-automatically from a specification. I will discuss two key new advances we have made: proof-theoretic synthesis, which produces a program along with its proof of correctness; and path-based inductive synthesis, which is able to compute inverses of programs. (3) Symbolic Execution. In this project, we are exploring ways to extend the power of symbolic execution by mixing it with static type systems and, separately, using it to understand software configuration spaces. Finally, although all three of these projects are quite diverse, they share some common ideas and insights that I will discuss throughout the talk.

I will conclude by discussing the future of research in this area and describing some new projects I am currently pursuing.