Automatic programming is the ultimate programmer’s dream: the programmer specifies what he wants (e.g., a sorting procedure), and the computer produces a program (e.g., the merge sort) that captures his intent. Realizing this dream requires the computer to synthesize an implementation and to verify its correctness—two tasks that are unachievable in a world of arbitrary programs and specifications. But in a finite world, which bounds the size of program executions and inputs, both synthesis and verification become search problems, mechanizable by reduction to satisfiability solving.

Yet building practical verification or synthesis tools is no easy task, even with the availability of high-performance solvers. Real applications require the underlying solver to explore astronomically large search spaces while looking for an implementation that satisfies a given specification (synthesis) or a program state that violates it (verification). As a result, straightforward reductions to satisfiability seldom scale in practice, and it takes months or years of expert work to build a practical tool for a new application domain.

In this talk, I will describe some of the solver-aided tools I have built over the years, the lessons I learned from these experiences, and their reflection in my current work on solver-aided languages. To successfully navigate massive search spaces, a tool needs to employ clever encodings and efficient code, but above all, it must expose the right abstractions. The right abstraction enables the tool’s client, be it a programmer or another tool, to provide domain-specific knowledge that can exponentially accelerate the underlying search. This acceleration, in turn, makes it possible to synthesize and verify real programs in a wide variety of application domains, from safety-critical software to router configuration to K-12 education. When such abstractions are built into a programming language, these benefits carry over to the task of creating the tools themselves, making it possible for every programmer to realize his own dream of automatic programming.

Emina Torlak is an Assistant Professor at the University of Washington, working at the intersection of programming languages, formal methods, and software engineering. She received her Bachelors (2003), Masters (2004), and Ph.D. (2009) degrees from MIT, and subsequently worked at IBM Research, LogicBlox, and as a research scientist at U.C. Berkeley. Her research aims to help people create better software more easily. As part of this agenda, she develops new languages and tools for computer-aided design, verification, and synthesis of software. Emina is the creator of the Kodkod constraint solver, which has been used in over 70 academic and industrial tools for software engineering. Her current work integrates constraint solvers into the Rosette programming language, which enables easy creation of solver-based tools for all kinds of systems, from radiotherapy machines to automated algebra tutors. Emina is a Sloan Research Fellow (2016) and a recepient of the AITO Dahl-Nygaard Junior Prize (2016).