11月22日：Xiaokang Qiu：Adaptive Concretization for Parallel Program Synthesis

报告题目: Adaptive Concretization for Parallel Program Synthesis

报告人：Xiaokang Qiu 教授

主持人：陈铭松

报告时间： 2016年11月22日14：00-15：30
报告地点：中北校区数学馆201

报告人简介：

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.

报告摘要：

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.