计算机工程2012，Vol.38Issue(22)：24-27,33,5.
符号执行中的循环依赖分析方法
Loop Dependence Analysis Method in Symbolic Execution
摘要
Abstract
Input-dependent loops can cause the problem of path explosion in symbolic execution, a method based on induction variable for analysis of loop dependence is proposed in this paper. By recognizing the loop induction variables and symbolic expressions, it is combined with the bound conditions to generate feasible path constraint for induction variable branches. Induction variable dependence of nested-loop is solved by symbolic affine analysis. It can generate test cases which can cover the branches of induction variables without loop unrolling. Test results show that by this method, two array access violations of the open source tools Libxml2 are found in while loops.关键词
符号执行/路径爆炸/归纳变量/循环依赖/约束求解/嵌套循环Key words
symbolic execution/ path explosion/ induction variable/ loop dependence/ constraint solving/ nested loop分类
信息技术与安全科学引用本文复制引用
刘杰,曹琰,魏强,彭建山..符号执行中的循环依赖分析方法[J].计算机工程,2012,38(22):24-27,33,5.基金项目
国家"863"计划基金资助项目(2008AA01Z420) （2008AA01Z420）
