Currrent Teaching

  • Spring 2017

    15-811: Verifying Complex Systems

    As the world increasingly depends on software, to control our finances, drive our cars, and manage our medical devices, how can we tell whether that software will be correct, secure, or reliable? Testing for such properties is notoriously difficult and ineffective. Software verification can, in principle, provide such guarantees, but verification has historically been difficult to apply at scale. A recent series of results, however, suggests we may be at an inflection point, as various research groups have successfully proven rigorous properties about critical software components, including OS kernels, compilers, cryptographic libraries, and distributed systems.

    15-811 focuses on these recent research results, though it also covers fundamentals of verification and includes a “bootcamp” tour of multiple verification tools.

Thesis Committees

  • Samee Zahur, University of Virginia. Defended April, 2016.
  • Srinath Setty, University of Texas, Austin. Defended August, 2014.
  • Yinqian Zhang, University of North Carolina. Defended June, 2014.

Teaching History

  • Spring 2016

    CSE 599W: Systems Verification

    CSE 599W was a special topics course on systems verification at the University of Washington. We examined research papers on applying formal verification techniques to building provably correct software, such as compilers, operating systems, Web browsers, and distributed systems. Co-taught with Zach Tatlock and Xi Wang.

  • Summer 2001

    English as a Second Language (ESL)

    Taught via Chester County OIC. Developed and implemented an English curriculum for a class of recent immigrants from Mexico, adapting instruction to accommodate a wide range of skill levels.