<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=gb2312"><meta name=Generator content="Microsoft Word 14 (filtered medium)"><style><!--
/* Font Definitions */
@font-face
{font-family:宋体;
panose-1:2 1 6 0 3 1 1 1 1 1;}
@font-face
{font-family:宋体;
panose-1:2 1 6 0 3 1 1 1 1 1;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:Tahoma;
panose-1:2 11 6 4 3 5 4 4 2 4;}
@font-face
{font-family:"\@宋体";
panose-1:2 1 6 0 3 1 1 1 1 1;}
@font-face
{font-family:微软雅黑;
panose-1:2 11 5 3 2 2 4 2 2 4;}
@font-face
{font-family:"\@微软雅黑";
panose-1:2 11 5 3 2 2 4 2 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
margin-bottom:.0001pt;
font-size:12.0pt;
font-family:宋体;}
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;
margin:0in;
margin-bottom:.0001pt;
font-size:12.0pt;
font-family:宋体;}
span.EmailStyle19
{mso-style-type:personal-reply;
font-family:"Calibri","sans-serif";
color:#44546A;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.25in 1.0in 1.25in;}
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:11.0pt;font-family:"Calibri","sans-serif";color:#44546A'>Please go to this talk if you are interested.<o:p></o:p></span></p><p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";color:#44546A'><o:p> </o:p></span></p><p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";color:#44546A'>Kenny<o:p></o:p></span></p><div><div style='border:none;border-top:solid #B5C4DF 1.0pt;padding:3.0pt 0in 0in 0in'><p class=MsoNormal><b><span style='font-size:10.0pt;font-family:"Tahoma","sans-serif"'>From:</span></b><span style='font-size:10.0pt;font-family:"Tahoma","sans-serif"'> chenyt@sjtu.edu.cn [mailto:chenyt@sjtu.edu.cn] <br><b>Sent:</b> Tuesday, November 22, 2016 3:29 PM<br><b>To:</b> all<br><b>Cc:</b> chenyt<br><b>Subject:</b> </span><span lang=ZH-CN style='font-size:10.0pt'>讲座通知：程序并行综合（普度大学邱晓康助理教授）</span><span style='font-size:10.0pt;font-family:"Tahoma","sans-serif"'><o:p></o:p></span></p></div></div><p class=MsoNormal><o:p> </o:p></p><div><p class=MsoNormal><span lang=ZH-CN style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black'>各位老师，</span><span style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black'><o:p></o:p></span></p></div><div><p class=MsoNormal><span style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black'><o:p> </o:p></span></p></div><div><p class=MsoNormal><span lang=ZH-CN style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black'>来自普度大学程序语言研究组的邱晓康助理教授在周三（</span><span style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black'>23<span lang=ZH-CN>日）</span><o:p></o:p></span></p></div><div><p class=MsoNormal><span lang=ZH-CN style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black'>上午</span><span style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black'>10<span lang=ZH-CN>点<span style='background:white'>在东上院</span></span><span style='background:white'>405<span lang=ZH-CN>教室介绍关于程序综合（</span>Program synthesis<span lang=ZH-CN>）</span></span><o:p></o:p></span></p></div><div><p class=MsoNormal><span lang=ZH-CN style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black;background:white'>方面的最新研究进展。</span><span style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black'><o:p></o:p></span></p></div><div><p class=MsoNormal><span style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black'><o:p> </o:p></span></p></div><div><p class=MsoNormal><span lang=ZH-CN style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black;background:white'>邱晓康博士毕业于美国</span><span style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black;background:white'>UIUC<span lang=ZH-CN>，博士毕业以后在美国</span>MIT CSAIL</span><span style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black'><o:p></o:p></span></p></div><div><p class=MsoNormal><span lang=ZH-CN style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black;background:white'>任博士后，</span><span style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black;background:white'>2016<span lang=ZH-CN>年起在普度大学程序语言研究组工作。邱晓康</span></span><span style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black'><o:p></o:p></span></p></div><div><p class=MsoNormal><span lang=ZH-CN style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black;background:white'>老师近几年在程序语言和软件工程的顶会（</span><span style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black;background:white'>POPL<span lang=ZH-CN>、</span>PLDI<span lang=ZH-CN>、</span>CAV<span lang=ZH-CN>、</span></span><span style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black'><o:p></o:p></span></p></div><div><p class=MsoNormal><span style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black;background:white'>ICSE<span lang=ZH-CN>、</span>FSE<span lang=ZH-CN>等）均有较强研究工作发表。</span></span><span style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black'><o:p></o:p></span></p></div><div><p class=MsoNormal><span style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black'><o:p> </o:p></span></p></div><div><p class=MsoNormal><span lang=ZH-CN style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black;background:white'>欢迎您和您的学生参加。</span><span style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black'><o:p></o:p></span></p></div><div><p class=MsoNormal><span style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black'><o:p> </o:p></span></p></div><div><p class=MsoNormal><span lang=ZH-CN style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black'>陈雨亭</span><span style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black'><o:p></o:p></span></p></div><div><p class=MsoNormal><span style='font-size:14.5pt;font-family:"微软雅黑","sans-serif";color:black'><o:p> </o:p></span></p></div><div><p class=MsoNormal style='text-align:justify;text-justify:inter-ideograph'><span style='font-family:"Calibri","sans-serif";color:black'>Title: Adaptive Concretization for Parallel Program Synthesis<o:p></o:p></span></p><p class=MsoNormal style='text-align:justify;text-justify:inter-ideograph'><span style='font-family:"Calibri","sans-serif";color:black'> <o:p></o:p></span></p><p class=MsoNormal style='text-align:justify;text-justify:inter-ideograph'><span style='font-family:"Calibri","sans-serif";color:black'>Abstract: Program synthesis tools work by searching for an implementation that satisfies a given specification. Two popular search strategies are symbolic search, which reduces synthesis to a formula passed to a SAT solver, and explicit search, which uses brute force or random search to find a solution. In this paper, we propose adaptive concretization, a novel synthesis algorithm that combines the best of symbolic and explicit search. Our algorithm works by partially concretizing a randomly chosen, but likely highly influential, subset of the unknowns to be synthesized. Adaptive concretization uses an online search process to find the optimal size of the concretized subset using a combination of exponential hill climbing and binary search, employing a statistical test to determine when one degree of concretization is sufficiently better than another. Moreover, our algorithm lends itself to a highly parallel implementation, further speeding up search.<o:p></o:p></span></p><p class=MsoNormal style='text-align:justify;text-justify:inter-ideograph'><span style='font-family:"Calibri","sans-serif";color:black'> <o:p></o:p></span></p><p class=MsoNormal style='text-align:justify;text-justify:inter-ideograph'><span style='font-family:"Calibri","sans-serif";color:black'>We implemented adaptive concretization for Sketch and evaluated it on a range of benchmarks. We found adaptive concretization is very effective, outperforming Sketch in many cases, sometimes significantly, and has good parallel scalability. As our algorithm involves a few tunable design decisions, we also systematically evaluate several dimensions of the design space to better understand the tradeoffs. We show that, in general, adaptive concretization is robust along those dimensions.<o:p></o:p></span></p><p class=MsoNormal style='text-align:justify;text-justify:inter-ideograph'><span style='font-family:"Calibri","sans-serif";color:black'> <o:p></o:p></span></p><p class=MsoNormal style='text-align:justify;text-justify:inter-ideograph'><span style='font-family:"Calibri","sans-serif";color:black'>Bio: Prof. Qiu is an Assistant Professor of Electrical and Computer Engineering at Purdue University. He finished his Ph.D. in Computer Science at the University of Illinois at Urbana-Champaign in 2013. Before starting at Purdue, he was a postdoctoral associate at the Massachusetts Institute of Technology. He is interested in software verification and synthesis, with a particular emphasis on heap-manipulating programs. His research focuses on program logics, decision procedures, automated verification, and syntax-guided synthesis. He is a member of the Purdue Programming Languages (PurPL) research group and leads the Computer-Aided Programming (CAP) group at Purdue.<o:p></o:p></span></p></div><p class=MsoNormal><span style='font-size:10.5pt;font-family:"微软雅黑","sans-serif";color:black'><o:p> </o:p></span></p></div></body></html>