University of Washington
My research aims to help people create better software more easily. As part of this agenda, I develop new languages and tools for computer-aided verification and synthesis of software. My collaborators and I apply these techniques to all kinds of systems, from radiotherapy machines to K-12 algebra tutors. A lot of our work is based on Rosette, a new language that makes it easy to create efficient tools for program verification, synthesis, and more.
First steps to adding the magic of SAT to your problem-solving toolbox.