Allen School professor Emina Torlak, co-founder of the UNSAT group and a member of the Programming Languages & Software Engineering (PLSE) group, earned the 2021 Robin Milner Young Researcher Award from the Association for Computing Machinery’s Special Interest Group on Programming Languages (ACM SIGPLAN) for her research contributions in automated reasoning to make computer programming easier. The award was named in honor of Milner, the legendary British computer scientist who was a leader in programming language research and had a passion for mentoring his younger colleagues. Torlak is the 10th recipient of the award, which is given to a researcher within 20 years of their start of graduate school.
“This prestigious award is explicit recognition of what is well-known in the programming-languages research community: Emina builds beautifully engineered systems that are ready for serious use not just by her group but by other researchers, and she does so by extending the elegant logical foundations of our field in sophisticated ways,” said Dan Grossman, professor and vice director of the Allen School. “Her tools don’t just work; they do things nobody else knows how to do.”
In her work, Torlak combines new language abstractions, algorithmic insights, robust design, and thorough implementation. From the start of her career as a doctoral student at MIT, she has been building tools and applications that find and solve problems in programming languages.
“Automatic verification of programs ensures that programs are free of bugs that hackers could exploit to break into the system. Unfortunately, verifying program correctness is a specialized task that programmers are not trained to perform,” said Allen School professor Rastislav Bodik. “Emina’s research goal has been to make automatic verification of programs accessible to programmers who lack expertise in verification. She has accomplished this vision by automating a lot of the verification process, in a clever way. Her key insight was that it was impossible to construct a super-verifier that would automatically verify all kinds of programs, and that to automate the process, verifiers would need to be tailored to narrower classes of programs. She designed a tool that allowed programmers to automatically construct such automatic verifiers for their programs.”
An example is Torlak’s Rosette framework, which allows users to quickly develop their own domain-specific program synthesis algorithms.
“Rosette is an ingenious design that combines advances from programming languages such as meta-programming, compilation as in partial evaluation and formal methods such as symbolic computation,” Bodik said. “Using Rosette, programmers were able to construct verifiers in a few days where it would take months to do so with traditional methods. Rosette was also used to construct synthesizers of programs, which are tools that automatically write programs. Using Rosette, researchers have built synthesizers that reached parity with human programming experts on a range of advanced programming tasks. This success owes both to Emina’s design skills and the leadership in supporting the open-source community around Rosette.”
Leveraging Rosette, Torlak helped to create Serval, a framework for creating automated verifiers for systems software. It overcomes several obstacles in scaling automated verification, including the developer effort required to write verifiers, the difficulty of finding and fixing performance bottlenecks, and limitations on their applicability to existing systems. From there, she contributed to the development of Jitterbug, a tool for writing and proving the correctness of just-in-time (JIT) compilers for computers using the extended Berkeley Packet Filter (eBPF) technology. It produces a formal correctness guarantee for eBPF JITs, a security-critical component of the Linux operating system, through a precise specification of JIT correctness and an automated verification strategy that scales to practical implementations.
“Emina Torlak is a leader in the area of automated verification. She has made both conceptual contributions and built tools that are state-of-the-art and widely used,” said the Milner Award selection committee. “On the conceptual side, the notion of a solver-aided programming language is hers and has quickly become standard terminology.”
Torlak’s research has been published at some of the most prestigious and highly competitive conferences in the field, including ACM SIGPLAN’s Symposium on Principles of Programming Languages (POPL), Conference on Programming Language Design and Implementation (PLDI), International Conference on Functional Programming (ICFP), International Conference on Computer Aided Verification (CAV), the International Conference on Software Engineering (ICSE) and much more. Torlak joined the University of Washington in 2014 and has since been named a Sloan Research Fellow and won an NSF CAREER Award, an Amazon Research Award, two Best Paper Awards, two Distinguished Paper Awards and a Distinguished Artifact Award.
Read more about Torlak’s Young Researcher Award here.
Congratulations, Emina!