摘要
随着软件规模的不断扩大以及复杂度的不断增长,人们越来越关注软件的可信性问题.验证程序是否满足断言所描述的性质,是保证软件可信性的一种常见方法.路径敏感的程序验证由于不可能遍历所有的路径,需要合并路径信息,因此造成精度上的损失.提出一种基于SMT求解器的路径敏感程序验证方法,在保证精确度的前提下,有效减少路径搜索空间.其基本思想是,利用最大强连通分量压缩循环路径,然后根据目标断言对控制流图进行切片.使用一种布尔表达式方法对路径空间进行抽象,结合抽象解释和符号执行技术对路径进行验证.结合F-Soft平台和Z3工具对该方法进行了实验验证,结果表明,该方法在验证的精确度和效率上都有较好的效果.
With the rapid increase in size and complexity of software,more and more attention is paid to the software’s trust.Verifying whether programs satisfy the properties described by assertions is a common method to guarantee trust of the software.Since path sensitive program verification cannot traverse all paths,it needs merge the path information,which causes a loss of precision.The study proposes a program verification method using SMT solvers,which can reduce the path search space and improve the precision at the same time.The method’s main sprit is impacting the cycle path by using maximal strongly connected component and slicing the CFG according to the aim assertion.The study abstracts the path space using Boolean formulas and verifies the path by combining abstract interpretation and symbolic execution.The study has conducted experiments based on the F-Soft program verification platform and SMT solver Z3,and results show that this method performs well based on precision and effect.
出处
《软件学报》
EI
CSCD
北大核心
2012年第10期2655-2664,共10页
Journal of Software
基金
国家自然科学基金(90818018
91018009)
关键词
路径敏感
程序验证
抽象解释
符号执行
SMT求解器
path sensitive
program verification
abstract interpretation
symbolic execution
SMT solvers
