Testing and other unsound analyses are developer-friendly but cannot give guarantees that programs are free of bugs. Verification and other extant sound approaches can give guarantees but often require too much effort for everyday developers. In this work, we describe our efforts to make verification more accessible for developers by using specialized pluggable typecheckers—a relatively accessible verification technology—to solve complex problems that previously required more complex and harder-to-use verification approaches.

I’m a Ph.D. student at the University of Washington Paul G. Allen School of Computer Science & Engineering. I work in the PLSE group on lightweight software verification. My advisor is Mike Ernst.

My current work is focused on building type systems on top of the Checker Framework to solve practical problems in software engineering.