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

[Kenny Zhu]

Please go to this talk if you are interested.

 

Kenny

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: 讲座通知：程序并行综合（普度大学邱晓康助理教授）

 

各位老师，

 

来自普度大学程序语言研究组的邱晓康助理教授在周三（23日）

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

方面的最新研究进展。

 

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

任博士后，2016年起在普度大学程序语言研究组工作。邱晓康

老师近几年在程序语言和软件工程的顶会（POPL、PLDI、CAV、

ICSE、FSE等）均有较强研究工作发表。

 

欢迎您和您的学生参加。

 

陈雨亭

 

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
search.

 

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>