实验室专题网站

友情链接

校内链接 校外链接

当前位置首页->新闻中心->新闻动态

计算机学院博士生谢肖飞获得ACM SIGSOFT 2016年度杰出论文奖

来源:
作者:
日期:2017-01-04 13:48:01

【字号

       我院李晓红教授及其指导的博士生谢肖飞,与新加坡南洋理工大学 Yang Liu助理教授以及博士后陈碧欢、美国爱荷华州立大学Wei Le助理教授合作研究的论文“Proteus: Computing Disjunctive Loop Summary via Path Dependency Analysis”被软件工程顶级会议FSE 2016 (24th ACM SIGSOFT International Symposium on the Foundations of Software Engineering) 所接收。鉴于该论文的研究针对符号执行中循环处理的难题,提出一种全新建模方法,可用于多个程序分析领域中,获得了ACM SIGSOFT 2016年度杰出论文奖,这是中国大陆学者首次获得该国际性奖项ACM SIGSOFT杰出论文奖(ACM Distinguished Paper Award)项授予在软件工程领域顶级会议ICSEASEFSE上发表的对软件工程发展有重大影响力的论文成果。

      循环分析在程序分析(例如程序验证,漏洞发现以及测试生成等)中一直是一个非常大的挑战。目前的研究主要依赖三种方法:循环展开,求不变量以及循环总结。循环展开最直接也最容易实现,但是展开的次数是不确定的,次数太少会导致不能正确的验证程序,或者漏掉一些bug和测试用例,次数太多又会导致程序分析花费大量的时间进行大量的循环展开。求循环不变量同样的也需要不断的展开循环以求得不动点,对于复杂的循环,例如多路径循环,通常会花费大量时间。而且如何保证求得的不变量足够强也是个很大的挑战。循环总结是一种可以获得更精确,更多信息的方法。在程序分析中,求得的循环总结可以用于替换循环以减少迭代循环带来的复杂度。然而对循环进行总结也是一个很有挑战的问题,已有的方法或者只能用于单路径的循环,或者求得的循环总结不够精确,使得很难用于已有的程序分析中。

      谢肖飞博士等从两方面去分析与提高循环分析。首先,通过对大量的(多路径)循环进行分析,提出了一种对循环进行分类的方法。该分类帮助理解循环分析的复杂度,即什么类型的循环可以被精确的总结,什么类型的循环可以通过一些近似的方法来进行总结以及什么类型的很难被总结。基于该分类,文中提出了一种新模型来对循环进行建模,该模型分析了多个路径间的依赖关系,从而解决了以往对多路径循环难以分析的问题;采用分而治之的方法,首先对每个路径分别进行总结,循环的某种执行的总结就是从初始路径到结束路径的总结累积,每条路径的准确性总结保证了循环总结的准确性。对于不能精确总结的循环,利用了一些现有的抽象技术来将其转换为可以总结的类型,虽然该类型的循环总结准确性降低,但依然可以被正确的用于程序验证,复杂度分析等多个领域。文中的分类方法对循环分析处理的研究具有较好的指导意义,研究成果可以直接用于编译器优化,程序验证,程序漏洞发现,测试用例生成,程序最坏执行时间分析以及程序性能分析等多个领域。

    该研究得到了国家科学基金(资助号61572349, 61272106)的资助。

      论文链接:http://dl.acm.org/citation.cfm?id=2950340

 

天津大学计算机科学与技术学院版权所有TEL:+86-022-27406538

天津博和利软件设计有限公司技术支持TEL:+86-022-27058558津ICP备05004161号