首页计算机学院研究生导师论坛和专题讲座
标题 Symbolic Verification of Regular Properties -- Guiding and Pruning
主讲人 陈振邦
职称
职位 国防科技大学计算机学院副教授,中国计算机协会形式化方法专委会委员
地点 计算机学院B404会议室
举办学院 计算机学院
举办时间 2018年5月18日10点正
主讲人简介 陈振邦,武汉黄陂人,博士,国防科技大学计算机学院副教授,中国计算机协会形式化方法专委会委员。分别于2002和2009年在国防科技大学获计算机科学与技术学士和博士学位,从2009年起于国防科技大学任教。目前主要的研究方向为程序分析、形式化方法及其在不同背景下的应用。相关研究成果发表在ICSE、FSE、FM、TCS、SCP等软件工程或形式化方法的会议或期刊上。2012年获国家科技进步二等奖1项,2018年获ICSE的杰出论文奖。担任过多个本方向国际国内学术会议的程序委员会委员,负责承担了多项自然科学基金项目,作为骨干参与多项包括973、863在内的国家重点项目。
讲座简介 正规性质是有限状态机(或正则表达式)可表达的性质。正规性质广泛应用于软件的规约、测试与验证等领域。程序正规性质的验证非常具有挑战。我们结合程序静态分析和动态分析技术,提出了基于动态符号执行的程序正规性质的符号化验证方法,包括面向正规性质的引导和路径削减方法,可快速找到满足正规性质的程序路径,完成程序路径空间的遍历。我们针对Java程序实现了原型工具,通过在实际开源Java程序上的实验表明,我们的方法在找到目标路径上有平均两个数量级的性能提升,在完成路径空间遍历上有平均一个数量级的性能提升。 该报告主要内容源自报告人的ICSE 2015、FSE 2017和ICSE 2018论文。