Write a Blog >>
PLDI 2021
Sun 20 - Sat 26 June 2021 PLDI
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

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.

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.

Fri 25 Jun

Displayed time zone: Eastern Time (US & Canada) change

15:00 - 16:00
KeynoteInvited Talks at PLDI-A +12h
Chair(s): Emery D. Berger University of Massachusetts Amherst
Robin Milner Young Researcher Award Presentation and Talk: Solver-Aided Programming for All
Invited Talks
Emina Torlak University of Washington

Sat 26 Jun

Displayed time zone: Eastern Time (US & Canada) change