Solver-aided tools have automated the verification and synthesis of practical programs in many domains, from high-performance computing to executable biology. These tools work by reducing verification and synthesis tasks to satisfiability queries, which involves compiling programs to logical constraints. Developing an effective symbolic compiler is challenging, however, and until recently, it took years of expert work to create a solver-aided tool for a new domain.

In this talk, I will present Rosette, a programming language for rapid creation of solver-aided tools. With Rosette, building these tools for a new domain is a matter of implementing a language for programming in that domain. Once you implement your domain-specific language (DSL), by writing a library or an interpreter, you get a symbolic compiler and the tools for free. This is made possible by Rosette’s symbolic virtual machine, which can translate both a DSL implementation and programs in that DSL to efficient constraints. Since its first public release in 2014, Rosette has enabled a wide range of programmers, from professional developers to high school students, to quickly create practical solver-aided tools for a variety of domains. Example applications include verifying radiation therapy software, generating tests for service-oriented architectures, and synthesizing custom tutoring rules for K-12 algebra. This talk will provide a brief introduction to Rosette and describe a few recent applications.

Emina Torlak is an Associate 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 focuses on developing automated tools and programming models for computer-aided design, verification, and synthesis of software. She is the creator of the Kodkod constraint solver, which has been used in over 70 academic and industrial tools for software engineering. Emina has applied her expertise to a broad range of problems, from verification of memory-consistency models to generation of test data for decision support applications. Her current work on the Rosette solver-aided language integrates constraint solvers into programming languages to support computer-aided verification, debugging, and synthesis of code, making programming a collaboration between humans and machines.