CSE2 201
Areas of interest: Compilers, 3D CAD, Verification, Synthesis

My goal is to help students become great computer scientists. On the research front, I work towards this goal with my students in PLSE and SAMPL. On the education front, I work towards this goal by teaching courses on programming languages and related topics.

My expertise is rooted in formal verification, especially of compilers. As my students develop their own research vision, we branch out across diverse domains. Our work is unified by themes of making it easier to write tricky code and figuring out how to ensure such programs are correct. We rigorously prove our results and always build real, working systems. Some of the domains we have explored include:

  • Compiler Optimization Synthesis
  • CAD Tools for 3D Printing and Carpentry
  • Automatic Numerical Accuracy Improvement
  • Machine Learning Compilers and Runtimes
  • Web Browser Layout Verification
  • Radiotherapy Control Verification
  • Distributed Systems Verification
  • Internet Router Verification

I can juggle and solve Rubik's cubes, but not at the same time.

Please see my homepage for more information.