[Adapt] FW: 讲座通知:程序并行综合(普度大学邱晓康助理教授)

Kenny Zhu kzhu at cs.sjtu.edu.cn
Tue Nov 22 15:40:59 CST 2016

Please go to this talk if you are interested.



From: chenyt at sjtu.edu.cn [mailto:chenyt at sjtu.edu.cn] 
Sent: Tuesday, November 22, 2016 3:29 PM
To: all
Cc: chenyt
Subject: 讲座通知:程序并行综合(普度大学邱晓康助理教授)





上午10点在东上院405教室介绍关于程序综合(Program synthesis)



邱晓康博士毕业于美国UIUC,博士毕业以后在美国MIT CSAIL









Title: Adaptive Concretization for Parallel Program Synthesis


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


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.


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.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://cs.sjtu.edu.cn/pipermail/adapt/attachments/20161122/d5091a99/attachment.html>

More information about the Adapt mailing list