Emina Torlak

A Tutorial on Solver-Aided Programming (CAV 2019)

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 presents 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. The tutorial provides a brief introduction to Rosette, describes a few recent applications, and aims to equip you with tools to build your own tools!

There are two parts to the tutorial, each with slides, notes, code examples, and exercises. The exercises will give you hands-on experience with the material covered in the tutorial, so trying them before looking at the solutions is highly recommended.

Part 1: getting started with solver-aided programming
slides, notes, code
exercises, solutions
Part 2: going pro with solver-aided programming
slides, notes, code
exercises, solutions