报告题目：Assertion Guided Symbolic Execution of Multithreaded Programs
报告日期及时间：2015-12-28 周一 9:30-10:20
报告地点： E202
报告人：杨子江
报告人单位：美国西密西根大学计算机科学系
报告人简介：杨子江博士现任西密西根大学计算机科学系副教授。他2003年从美国宾夕法尼亚大学计算机与信息科学系获得博士学位，1999年从美国赖斯大学计算机科学系获得硕士学位，1996年从中国科技大学计算机系获得学士学位并获得该校最高荣誉郭沫若奖学金。杨子江博士目前主要从事软件测试及验证领域的研究。迄今为止发表了六十余篇论文及十项美国专利。他获得2008年度ACM TODAES最佳期刊论文奖, 2010年PADTAD最佳会议论文奖，2008年西密西根大学工学院研究成就奖，和2015年谷歌CS Engagement奖。杨子江博士是国际电子电气工程师协会资深会员，并担任过密西根大学电子与计算机科学系访问教授，NEC公司美国研发中心科研顾问，美国自然科学基金评委，美国宇航局博士后评委，美国能源部科技企业基金评委等职。
报告摘要：
Symbolic execution has emerged as a powerful technique for systematic testing of sequential and multithreaded programs. However, its application is limited by the high computational cost of covering all feasible intra-thread paths and inter-thread interleavings. We propose a new assertion guided pruning framework that identifies executions guaranteed not to lead to an error state and removes them during symbolic execution. By summarizing the reasons why previously explored executions cannot reach an error state and using the information to prune redundant executions in the future, we can soundly reduce the search space exponentially. We also use static concurrent program slicing and heuristic minimization of symbolic constraints to further reduce the computational overhead. We have implemented our method in the Cloud9 symbolic execution tool and evaluated it on a large set of multithreaded C/C++ programs. Our experiments show that the new method can reduce the overall computational cost significantly. The findings of this work have been presented at FSE’15.
邀请人：刘进 教授
