<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40"><head><meta http-equiv=Content-Type content="text/html; charset=utf-8"><meta name=Generator content="Microsoft Word 15 (filtered medium)"><style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
margin-bottom:.0001pt;
font-size:12.0pt;
font-family:"Times New Roman",serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#0563C1;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:#954F72;
text-decoration:underline;}
p
{mso-style-priority:99;
mso-margin-top-alt:auto;
margin-right:0in;
mso-margin-bottom-alt:auto;
margin-left:0in;
font-size:12.0pt;
font-family:"Times New Roman",serif;}
p.msonormal0, li.msonormal0, div.msonormal0
{mso-style-name:msonormal;
mso-margin-top-alt:auto;
margin-right:0in;
mso-margin-bottom-alt:auto;
margin-left:0in;
font-size:12.0pt;
font-family:"Times New Roman",serif;}
span.EmailStyle19
{mso-style-type:personal;
font-family:"Calibri",sans-serif;
color:#1F497D;}
span.EmailStyle20
{mso-style-type:personal-compose;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
{page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]--></head><body lang=EN-US link="#0563C1" vlink="#954F72"><div class=WordSection1><p class=MsoNormal><span style='font-size:13.5pt;font-family:"Calibri",sans-serif;color:black'>PL Seminar Speaker</span><span style='color:black'><o:p></o:p></span></p><div><p class=MsoNormal><span style='font-size:13.5pt;font-family:"Calibri",sans-serif;color:black'> </span><span style='color:black'><o:p></o:p></span></p></div><div><p class=MsoNormal><span style='font-size:13.5pt;font-family:"Calibri",sans-serif;color:black'>Armando Solar-Lezama, from MIT</span><span style='color:black'><o:p></o:p></span></p></div><div><p class=MsoNormal><span style='font-size:13.5pt;font-family:"Calibri",sans-serif;color:black'>Wednesday, November 14 - 3:00 pm</span><span style='color:black'><o:p></o:p></span></p></div><div><p class=MsoNormal><span style='font-size:13.5pt;font-family:"Calibri",sans-serif;color:black'>Computer Science - Room 302</span><span style='color:black'><o:p></o:p></span></p><p class=MsoNormal><span style='color:black'><o:p> </o:p></span></p></div><div><p style='margin:0in;margin-bottom:.0001pt'><b><span style='font-size:13.5pt;font-family:"Calibri",sans-serif;color:black'>Formal Methods meets ML: Synthesis, Verification and Beyond</span></b><span style='font-family:"Calibri",sans-serif;color:black'><o:p></o:p></span></p><p class=MsoNormal><span style='font-family:"Calibri",sans-serif;color:black'><o:p> </o:p></span></p><p style='margin:0in;margin-bottom:.0001pt'><span style='font-size:13.5pt;font-family:"Calibri",sans-serif;color:black'>In this talk I will describe some recent work in my group that brings together machine learning and formal methods. The talk will describe both how formal methods can feed off from each other to the benefit of both. Specifically, I will highlight three recent projects where the interaction of the two leads to new capabilities for both. First, I will talk about how ideas from AI and Machine learning can benefit program synthesis and lead to synthesis systems that are more flexible and easier to develop. I will also describe how ideas from formal methods can be used both to verify machine learning systems and to gain a better understanding of their behavior.</span><span style='font-family:"Calibri",sans-serif;color:black'><o:p></o:p></span></p><p class=MsoNormal><span style='font-family:"Calibri",sans-serif;color:black'><o:p> </o:p></span></p><p style='margin:0in;margin-bottom:.0001pt'><span style='font-size:13.5pt;font-family:"Calibri",sans-serif;color:black'>Bio: Armando Solar-Lezama is an associate professor in the department of electrical engineering and computer science at MIT. He leads the Computer Aided Programming group, which has been working on the application of learning and automated reasoning to automate challenging aspects of programming.</span><span style='font-family:"Calibri",sans-serif;color:#1F497D'><o:p></o:p></span></p></div></div></body></html>