BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Solver-Aided Programming for All
DTSTART:20190822T101500
DTEND:20190822T111500
DTSTAMP:20260428T214819Z
UID:c40cb0cc08d1971352e4c1871114f78139e7892c08a044e6bb45a948
CATEGORIES:Conferences - Seminars
DESCRIPTION:By Emina Torlak\n\nAbstract\nSolver-aided tools have automated
  the verification and synthesis of practical programs in many domains\, fr
 om high-performance computing to executable biology. These tools work by r
 educing verification and synthesis tasks to satisfiability queries\, which
  involves compiling programs to logical constraints. Developing an effecti
 ve symbolic compiler is challenging\, however\, and until recently\, it to
 ok years of expert work to create a solver-aided tool for a new domain.\n\
 nIn this talk\, I will present Rosette\, a programming language for rapid 
 creation of solver-aided tools. With Rosette\, building these 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 writin
 g a library or an interpreter\, you get a symbolic compiler and the tools 
 for free. This is made possible by Rosette's symbolic virtual machine\, wh
 ich can translate both a DSL implementation and programs in that DSL to ef
 ficient 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 va
 riety of domains. Example applications include verifying radiation therapy
  software\, generating tests for service-oriented architectures\, and synt
 hesizing custom tutoring rules for K-12 algebra. This talk will provide a 
 brief introduction to Rosette and describe a few recent applications.\n\nB
 io\nEmina Torlak is an Associate Professor at the University of Washington
 \, working on new languages and tools for computer-aided design\, verifica
 tion\, and synthesis of software. She received her Bachelors (2003)\, Mast
 ers (2004)\, and Ph.D. (2009) degrees from MIT\, and subsequently worked a
 t 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 7
 0 academic and industrial tools for software engineering. Her work on the 
 Rosette system integrates solvers programming languages\, enabling program
 mers to create their own solver-aided tools for all kinds of systems\, fro
 m radiotherapy machines to automated algebra tutors. Emina is a recipient 
 of the NSF CAREER Award (2017)\, Sloan Research Fellowship (2016)\, and th
 e AITO Dahl-Nygaard Junior Prize (2016).\n\nMore information\n\nhttps://me
 diaspace.epfl.ch/media/0_kf9vuw58\n\n\n 
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR