Robin Milner Young Researcher Award Presentation and Talk: Solver-Aided Programming for All (PLDI 2021 - Invited Talks)

Track

PLDI 2021 Invited Talks

Time Zone

The program is currently displayed in (GMT-04:00) Eastern Time (US & Canada).

Use conference time zone: (GMT-04:00) Eastern Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Fri 25 Jun 2021 15:00 - 16:00 at PLDI-A - Keynote Chair(s): Emery D. Berger
Sat 26 Jun 2021 03:00 - 04:00 at PLDI-A - Keynote

Abstract

The Robin Milner Young Researcher Award is given by ACM SIGPLAN to recognize outstanding contributions by young investigators in the area of programming languages.

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.

This talk presents Rosette, a programming language for rapid creation of solver-aided tools. To build a new tool, you write an interpreter for the tool’s input language, and Rosette lifts this interpreter into a symbolic compiler. The lifting is made possible by Rosette’s symbolic virtual machine, which can translate both a language implementation and programs in that language 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 create over 30 new verification and synthesis tools. Example applications include verifying radiation therapy software in current clinical use, synthesizing GPU kernels, and verifying and synthesizing just-in-time compilers that are part of the Linux operating system. This talk will provide a brief introduction to Rosette and describe recent applications.

Bio

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.