Synthesis and verification are revolutionizing the way we program. They are helping us create programs that run on energy-efficient hardware, that grade student work and provide feedback, and that automate end-user programming by example. But these tools are very hard to build—today, all of them are made by highly skilled researchers with expertise in many fields, from formal methods to programming languages to software engineering.

In this talk, I present a new approach to constructing tools for synthesis and verification that requires little beyond modern programming skills. The approach is based on two observations. First, much of everyday programming involves the use of domain-specific languages (DSLs) that are embedded, in the form of APIs and interpreters, into modern host languages (for example, JavaScript, Scala or Racket). Second, productivity tools based on constraint solvers (such as verification or synthesis) work best when specialized to a given domain. Rosette is a new kind of host language, designed for easy creation of DSLs that are equipped with solver-based tools. These Solver-Aided DSLs (SDSLs) use Rosette’s symbolic virtual machine (SVM) to automate hard programming tasks, including verification, debugging, synthesis, and programming with angelic oracles. The SVM works by compiling SDSL programs to logical constraints understood by SMT solvers, and then translating the solver’s output to counterexamples (in the case of verification), traces (in the case of angelic execution), or code snippets (in the case of synthesis and debugging). Rosette has hosted several new SDSLs, including imperative SDSLs for data-parallel and spatial programming; a functional SDSL for specifying executable semantics of secure stack machines; and a declarative SDSL for web scraping by example.

Track: ECOOP Summer School

Emina Torlak is an Assistant Professor at the University of Washington, working at the intersection of software engineering, programming languages, and formal methods. 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 that help people build better software more easily. 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 integrates constraint solvers into programming languages to support computer-aided verification, debugging, and synthesis of code, making programming a collaboration between humans and machines.