[PRL] colloquium today

[Matthias Felleisen]

Everyone, this is really a PRL talk turned into a departmental colloquium. Please participate -- Matthias





Begin forwarded message:

> From: Jessica Biron <bironje at ccs.neu.edu>
> Subject: [professors] [Colloq] Colloquium Talk - Growing Solver-Aided Languages with Rosette - Torlak - April 8th, 11:45am, 366 WVH
> Date: April 8, 2013 9:48:08 AM EDT
> To: colloq <colloq at lists.ccs.neu.edu>
> 
> 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/ 
> _______________________________________________
> Colloq mailing list
> Colloq at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/colloq