期刊文献+

符号执行中非线性归纳变量循环优化分析方法 被引量:1

Optimization and Analysis of the Non-Linear Induction Variable Loop in Symbolic Execution
下载PDF
导出
摘要 提出了一种新型的循环优化分析方法,用于在符号执行中优化归纳变量为非线性的循环。首先详细分析了非线性归纳变量在符号执行中产生的问题,通过将循环内部变量转换为递推链CR基本式,推导得出的归纳变量与循环次数的依赖式,进而采用二次曲面拟合的方法对其进行化简,从而达到了循环优化的方法,实验证明文章提出的方法在一定程度上缓解了非线性归纳变量给符号执行带来的状态空间爆炸、死循环等问题。 This paper proposes a new method of loop optimization and analysis during the symbolic execution,which could optimize the non-linear induction variable loop.This paper first analyses the issues that the loop brings,then uses the Chains of Recurrence Algebra to turn the non-linear induction variable into the CR form,and the optimization method is based on the conicoid.The issues such as state space explosion and infinite loop can be eased effectually.
出处 《信息工程大学学报》 2017年第5期630-634,共5页 Journal of Information Engineering University
关键词 递推链代数 循环优化 符号执行 chains of recurrence algebra loop optimization symbolic execution
  • 相关文献

参考文献4

二级参考文献59

  • 1Zhang Jian, Wang Xiao-Xu. A constraint solver and its application to path feasibility analysis. International Journal of Software Engineer and Knowledge Engineer, 2001, 11 (2) : 139-156.
  • 2Beizer B. Software Testing Techniques. New York, NY, USA: John Wiley & Sons, Inc. , 1989.
  • 3Zhang Jian. Symbolic execution of program paths involving pointer and structure variables//Proceedings of the 4th International Conference on Quality Software (QSIC2004). IEEE Computer Society, Braunschweig, Germany, 2004:87-92.
  • 4Ruan Hui, Zhang Jian, Yan Jun. Test data generation for C programs with string-handling functions//Proceedings of the 2nd IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE2008). Nanjing, China: IEEE Computer Society, 2008:219-226.
  • 5Velroyen H. Automatic non-termination analysis of imperative programs [M. S. dissertation]. Chalmers University of Technology, Goteborg, 2007.
  • 6Bradley A, Manna Z, Sipma H. Linear ranking with reachability//Proceedings of the 17th International Conference on Computer Aided Verification (CAV 2005). Edinburgh, Scot land, UK, 2005:491-504.
  • 7Bradley A, Manna Z, Sipma H. The polyranking principle// Proceedings of 32nd International Colloquium on Automata, Language and Programming (ICALP 2005). Lisbon, Portugal, 2005:1349-1361.
  • 8Yang Lu, Zhan Naijun, Xia Bican, Zhou Chaochen. Program verification by using DISCOVERER//Proceedings of the first International Conference on Verified Software: Theories, Tools, Experiments (VSTTE 2005). Zurich, Switzerland, 2005:528-538.
  • 9Cook B, Podelski A, Rybalchenko A. Abstraction refinement for termination//Proceedings of the 12th International Symposium on Static Analysis (SAS 2005). London, UK, 2005: 87-101.
  • 10Rodriguez Carbonell E, Kapur D. Program verification using automatic generation of invariants//Proceedings of the 1st International Colloquium on Theoretical Aspects of Computing(ICTAC 2004). Guiyang, China, 2004:325-340.

共引文献8

同被引文献4

引证文献1

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部