Emina Torlak

Photo of Emina by Dennis Wise

Assistant Professor
Computer Science
University of Washington

CSE 596

Rosette GitHub
DBLP GoogleScholar


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.


28 Sep 2017

Our paper on symbolic types for lenient symbolic execution will appear at POPL 2018.

19 Sep 2017

Our paper on push-button verification of an OS kernel will appear at SOSP 2017.

23 Jun 2017

A Primer on Boolean Satisfiability

First steps to adding the magic of SAT to your problem-solving toolbox.

20 Jun 2017

Our paper on synthesizing puzzle-solving strategies will appear at FDG 2017.

05 Jun 2017

Our paper on the SpaceSearch library for building verified solver-aided tools will appear at ICFP 2017.

See all posts.