<html><head><style type='text/css'>p { margin: 0; }</style></head><body><div style='font-family: arial,helvetica,sans-serif; font-size: 12pt; color: #000000'><p class="page__title title" id="page-title"><font size="3">Programming for Everyone: From Solvers to Solver-Aided Languages and Beyond</font></p><div><p><font size="3"><span class="event-speaker">
<a href="http://people.csail.mit.edu/emina/">Emina Torlak</a> </span>
<span class="event-speaker-from">
(<a href="http://www.eecs.berkeley.edu">University of California, Berkeley</a>)
<br>Monday, March 31, 4:30pm<br>Computer Science 105<br><br></span><br>We live in a software-driven world. Software helps us communicate
and collaborate; create art and music; and make discoveries in
biological, physical, and social sciences. Yet the growing demand for
new software, to solve new kinds of problems, remains largely unmet.
Because programming is still hard, developer productivity is limited,
and so is end-users' ability to program on their own.
</font></p><div><p><font size="3"> </font></p></div><p>
</p><div><p><font size="3">In this talk, I present a new approach to constructing programs,
which exploits advances in constraint solving to make programming easier
for experts and more accessible to everyone else. The approach is
based on two observations. First, much of everyday programming involves
the use of domain-specific languages (DSLs) that are embedded, in the
form of APIs and interpreters, into modern host languages (for example,
JavaScript, Scala or Racket). Second, productivity tools based on
constraint solvers (such as verification or synthesis) work best when
specialized to a given domain. Rosette is a new kind of host language,
designed for easy creation of DSLs that are equipped with solver-based
tools. These Solver-Aided DSLs (SDSLs) use Rosette's symbolic virtual
machine (SVM) to automate hard programming tasks, including
verification, debugging, synthesis, and programming with angelic
oracles. The SVM works by compiling SDSL programs to logical
constraints understood by SMT solvers, and then translating the solver's
output to counterexamples (in the case of verification), traces (in the
case of angelic execution), or code snippets (in the case of synthesis
and debugging). Rosette has hosted several new SDSLs, including
imperative SDSLs for data-parallel and spatial programming; a functional
SDSL for specifying executable semantics of secure stack machines; and a
declarative SDSL for web scraping by example.</font></p></div><p>
</p><div><p>
</p><div><p><font size="3"> </font></p></div><p>
</p><div><p><font size="3"><span style="font-size:13px">Emina Torlak is a researcher at U.C.
Berkeley, working at the intersection of software engineering, formal
methods, and programming languages. Her focus is on developing tools
that help people build better software more easily. She received her
B.Sc. (2003), M.Eng. (2004) and Ph.D. (2009) from MIT, where she
developed Kodkod, an efficient SAT-based solver for relational logic.
Kodkod has since been used in over 70 tools for verification,
debugging, and synthesis of code and specifications. Emina has also
worked on a wide range of domain-specific formal methods. She won an
ACM SIGSOFT distinguished paper award for her work at LogicBlox, where
she built a system for synthesizing massive data sets, used in testing
of decision support applications. As a member of IBM Research, she led
the development of a tool for bounded verification of memory models,
enabling the first fully automatic analysis of the Java Memory Model.
These experiences inspired her current research on solver-aided
languages, which aims to reduce the effort of applying formal methods to
new problem domains.</span> </font></p></div><p>
</p></div><p><font size="3"><br><span name="x"></span><br></font></p></div><p></p></div></body></html>