[Colloq] Colloquium Talk - Growing Solver-Aided Languages with Rosette - Torlak - April 8th, 11:45am, 366 WVH

[Jessica Biron]

Please join us for a Colloquium Talk by Emina Torlak, UC Berkeley 

Monday, April 8th 
11:45am 
366 WVH 

Decision procedures have helped automate key aspects of programming: coming up with a code fragment that implements a desired behavior (synthesis); establishing that an implementation satisfies a desired property (code checking); locating code fragments that cause an undesirable behavior (fault localization); and running a partially implemented program to test its existing behaviors (angelic execution). Each of these aspects is supported, at least in part, by a family of formal tools. Most such tools are built on infrastructures that are tailored for a particular language or purpose, e.g., Boogie for verification and Sketch for synthesis of C-like languages. But so far, no single infrastructure provides a platform for automating the full spectrum of programming activities, or for making such automation easily available in new languages and programming models. 

This talk introduces Rosette, a new shared infrastructure for designing and growing solver-aided languages. The Rosette system is itself a solver-aided EDSL (embedded domain-specific language), which inherits and exposes extensive support for meta programming from its host language, Racket. The system works through a combination of program transformation (enabled by Racket’s meta-programming facilities) and symbolic execution, in which programming constructs and operators accept both concrete and symbolic values. With our framework, a designer defines a new solver-aided language by simply writing an interpreter for it in Rosette. Such a language will allow some constructs to be underspecified---that is, to produce symbolic "holes" rather than just concrete values. When a program with holes and the language interpreter are compiled with Rosette, the result is a custom symbolic execution engine for the given program and language. Executing this engine yields an encoding of the program’s semantics as a set of constraints, which are then solved by an off-the-shelf decision procedure to discharge synthesis, verification, and other queries about the program. We show how to use Rosette to prototype a tiny DSL with a program checker, a fault localizer, an angelic oracle, and 
an inductive synthesizer. 




Jessica Biron 
Administrative Assistant – Office of the Dean and CCIS Development 
College of Computer and Information Science 
Northeastern University 
202 West Village H 
617-373-5204 
bironje at ccs.neu.edu 
http://www.ccs.neu.edu/