5月15日学术报告(西密西根大学:杨子江)

5月15日学术报告(西密西根大学:杨子江)

类别：网络整理发布人：admin 浏览次数：次发布时间：2015-09-02 14:25

报告题目：Post-conditioned Symbolic Execution

报告日期及时间：2015-5-15 周五 10:00-10:45

报告地点： B403

报告人：杨子江副教授

报告人单位：西密西根大学计算机科学系

报告人简介：
杨子江博士现任西密西根大学计算机科学系副教授。他2003年从美国宾夕法尼亚大学计算机与信息科学系获得博士学位，1999年从美国赖斯大学计算机科学系获得硕士学位，1996年从中国科技大学计算机系获得学士学位并获得该校最高荣誉郭沫若奖学金。杨子江博士目前主要从事软件测试及验证领域的研究。迄今为止发表了六十余篇论文及十项美国专利。他获得2008年度ACM TODAES最佳期刊论文奖, 2010年PADTAD最佳会议论文奖，2008年西密西根大学工学院研究成就奖，和2015年谷歌CS Engagement奖。杨子江博士是国际电子电气工程师协会资深会员，并担任过密西根大学电子与计算机科学系访问教授，NEC公司美国研发中心科研顾问，美国自然科学基金评委，美国宇航局博士后评委，美国能源部科技企业基金评委等职。

报告摘要：
Symbolic execution is emerging as a powerful technique for generating test inputs systematically to achieve exhaustive path
coverage of a bounded depth. However, its practical use is often limited by path explosion because the number of paths of a
program can be exponential in the number of branch conditions encountered during the execution. To mitigate the path
explosion problem, we propose a new redundancy removal method called post conditioned symbolic execution. At each
branching location, in addition to determine whether a particular branch is feasible as in traditional symbolic execution, our
approach checks whether the branch is subsumed by previous explorations. This is enabled by summarizing previously explored
paths by weakest precondition computations. Post conditioned symbolic execution can identify path suffixes shared by multiple
runs and eliminate them during test generation when they are redundant. Pruning away such redundant paths can lead to a
potentially exponential reduction in the number of explored paths. We have implemented our method in the symbolic execution
engine KLEE and conducted experiments on a large set programs from the GNU Coreutils suite. Our results confirm that
redundancy due to common path suffix is both abundant and widespread. The findings of this work have been presented at
ICST’15.

邀请人：刘进教授

上一篇：5月14日学术报告(University of Melbourne:Dr. Rajkumar)

下一篇：12月26日学术报告（清华大学毕军：未来互联网/SDN的发展及其思考）