Spotlight: Emina Torlak

I will be joining the University of Washington this fall, but I am currently a researcher at U.C. Berkeley.  Before that, I was a Senior Computer Scientist at LogicBlox, a Research Staff Member at IBM, and a graduate, masters, and undergraduate student at MIT.  I work at the intersection of software engineering, formal methods, and programming languages.  My focus is on developing tools and methodologies that help people build better software more easily.  As part of my thesis, I developed Kodkod, an efficient SAT-based solver that has been used in over 70 automated tools for program verification, debugging, and synthesis.  At IBM, I led the development of a tool for bounded verification of memory consistency models, enabling the first fully automatic analysis of the Java Memory Model.  At LogicBlox, I built an award-winning system for synthesizing massive data sets, used in performance testing of decision support applications.  These experiences inspired my current research on solver-aided languages, which aims to reduce the effort of applying automated reasoning to new problem domains.

I like to work on practical problems that require both theoretical insights and engineering.  When looking for solutions, my guiding principles are elegance of ideas and simplicity of implementation.  I am excited about developing new knowledge and tools to automate the mechanics of programming (such as searching for bugs or for code snippets that implement specific behaviors), so that people can focus their efforts on creative tasks—coming up with designs, insights, properties, and examples.

If I had to pick one, it would be my latest paper with Ras Bodik, published at PLDI 2014:  “A lightweight symbolic virtual machine for solver-aided host languages.”  In this paper, we present a new lightweight technique for translating programs into logical constraints, which we call a symbolic virtual machine (SVM).  The SVM enables easy creation of domain-specific languages (DSLs) that are equipped with advanced automated tools, ranging from verification to synthesis.  Usually, building such tools involves translating DSL programs to constraints understood by SAT or SMT solvers.  Given these constraints, solvers then search for bad inputs (in the case of verification) or for code (in the case of synthesis). Our approach eliminates the need for DSL designers to translate their languages to constraints.  All they need to do is implement their DSLs, by writing an interpreter or a library, in a host language that is equipped with an SVM.  The host’s SVM reduces to constraints both the DSL implementation and programs in that DSL.  Our paper describes how the SVM does this efficiently, and how to build an SVM without a heroic engineering effort that is normally required for translating advanced general purposes languages, such as a host language, to constraints.  We also present our own solver-aided host language, Rosette, which implements these ideas and is host to four new solver-aided DSLs.

Several, all focused on moving computer-aided programming into the mainstream development workflow.  Tools for synthesis, verification, etc., are already being used in specialized domains (e.g., in the development of low-level device drivers or creation of signal processing libraries).  Programmers adopt these tools because they offer a clear advantage over unaided development, such as increased productivity, reliability, or performance.  But tools that meet the adoption bar generally take years to tune and develop.  I am interested in finding out how we can build highly usable and useful automation with exponentially less effort—imagine being able to produce a code-completion assistant or a bug finder for your project in just a few hours!  Solver-aided languages, like Rosette, take us one step closer to this goal.  To go further, I plan to explore ways to make solver-aided automation more interactive and more tuned to a given domain.  For example, a solver-aided tool works by exploring enormous search spaces with the help of SAT or SMT solvers, which rely on effective search heuristics.  When these heuristics break down, the tool should be able to explain to the programmer why it is getting stuck (e.g., perhaps the problem has too many symmetries) and even suggest what additional knowledge (e.g., an invariant) would help it proceed.  Such an interactive development model has been successfully applied to optimizing compilers, which suggests that programmers are willing to interact with their tools for a large-enough payoff.  Another promising direction is to base domain-specific tools on specialized solvers, which brings up the problem of how to mechanize the production of solvers and solving heuristics.

What I like most about PL research is its combination of depth of techniques and breadth of applications.  PL techniques such as verification and synthesis have been applied to a wide variety of non-PL fields, including networking, security, biology, social sciences, and many more.  Thanks to this, specialized technical results in PL can have broad practical impact, and as PL researchers, we have the opportunity to contribute not to just our own field but to many others as well.  This is also what I like about the PL community—our openness to new ideas, new application domains, and newcomers.

More demos, more applications, and more outreach efforts, like this blog.  As a community, we could be better at explaining to the rest of the world what it is that we do and why it matters.  I would like to see both more formal outreach, through our undergraduate curriculums, and more informal outreach, through practical applications and demonstrations of all the great work that we are doing.  The HCI, AI, and CG communities are very good at this, and we can learn a lot from them.

What advice would you have for graduate students who want a faculty job in the next couple of years?