My research focuses on improving software reliability and security. Toward that end, I have developed several new techniques to ensure program correctness and security in domains ranging from compilers to web browsers. My work draws upon interactive theorem provers like Coq and automated tools like Satisfiability Modulo Theories (SMT) solvers in order to make strong, formal correctness guarantees. Using these tools, I develop techniques to verify real software systems at scale and also to make verification accessible to non-expert programmers. As a graduate student at UCSD, I have enjoyed several opportunities to teach and mentor both undergraduate and graduate students. I have developed my own lecture material on a variety of programming language topics, designed course projects at the graduate and undergraduate levels, and have advised undergraduates interested in pursuing graduate studies. During the past year, I have also closely mentored junior graduate students who are tackling a large research project with the Coq interactive theorem prover.