Solver-Aided Programming, Emina Torlak, University of Washington
Time: Sunday, July 14, 09:00-10:30 and 11:00-12:30
Abstract: 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 (bounded) 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 tutorial will present Rosette, a programming language for rapid creation of solver-aided tools. With Rosette, building such tools for a new domain is a matter of implementing a language for programming in that domain. Once you implement your domain-specific language (DSL), by writing a library or an interpreter in Rosette, you get a symbolic compiler and the tools for free. This is made possible by Rosette’s symbolic virtual machine, which can translate both a DSL implementation and programs in that DSL 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 quickly create practical solver-aided tools for a variety of domains. Example applications include verifying radiation therapy software, generating efficent code for ultra low-power hardware, and synthesizing custom tutoring rules for K-12 algebra. This tutorial will provide a brief introduction to Rosette, describe a few recent applications, and equip you with tools to build your own tools!
Bio: Emina Torlak is an Associate Professor at the University of Washington, working on new languages and tools for computer-aided design, verification, and synthesis of software. 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. Emina is the creator of the Kodkod solver, which has been used in over 70 academic and industrial tools for software engineering. Her current work integrates solvers into the Rosette programming language, enabling programmers to create their own solver-aided tools for all kinds of systems, from radiotherapy machines to automated algebra tutors. Emina is a recipient of the NSF CAREER Award (2017), Sloan Research Fellowship (2016), and the AITO Dahl-Nygaard Junior Prize (2016).
Verification with Refinement Types, Ranjit Jhala, UC San Diego
Time: Sunday, July 14, 14:30-16:00 and 16:30-18:00
Abstract: The last few decades have seen tremendous strides in various technologies for reasoning about programs. However, we believe these technologies will only become ubiquitous if they can be seamlessly integrated within programming so that programmers can use them continuously throughout the software development lifecycle. In this tutorial, we will learn how refinement types offer a path towards integrating verification into existing host languages, by integrating the compositional nature of types with the expressiveness of logics, and the automation of model checking. We will see how refinements allow the programmer to extend specifications using types, to extend the analysis using SMT and abstract interpretation and finally, to extend verification beyond automatically decidable logical fragments, by allowing programmers to interactively write proofs simply as code in the host language.
The tutorial will include hands-on exercises, so bring your laptops!
Bio: Ranjit Jhala is a professor of Computer Science and Engineering at the University of California, San Diego. He works on algorithms and tools that help engineer reliable computer systems. His work draws from and contributes to the areas of Model Checking, Program Analysis, and Automated Deduction, and Type Systems. He is proud to have written some of the most cited papers in Programming Languages over the last twenty years, and even more to have helped create several influential and award winning systems including the BLAST software model checker, RELAY race detector, MACE/MC distributed language and model checker, and Liquid Types. He was awarded ACM SIGPLAN’s Robin Milner Young Researcher Award in 2018.