中国科学院重庆绿色智能技术研究院机构知识库

QQ客服 官方微博 反馈留言

	基于dixon结式和逐次差分代换的多项式秩函数探测方法
	袁月1; 李轶2
	2019
摘要	秩函数探测是循环程序终止性分析的重要方法,目前,已有很多研究者致力于为线性循环程序探测对应的线性秩函数,然而,针对具有多项式循环条件和多项式赋值的多项式型的循环,现有的秩函数探测方法还有所不足,解决方案大多是不完备的、或者具有较高的时间复杂度。针对现有工作对于多项式秩函数探测方法不足的问题,基于扩展Dixon结式( KSY方法)和逐次差分代换( SDS)方法,提出一种为多项式循环程序探测多项式型秩函数的方法。首先,将待探测的秩函数模板看作带参数系数的多项式,将秩函数的探测转换为寻找满足条件的参数系数的问题;然后,进一步将问题转换为判定相应的方程组是否有解的问题,至此,利用KSY方法中的扩展的Dixon结式,将问题更进一步简化为带参系数多项式(即结式)严格为正的判定问题;最后,利用SDS方法,找到一个充分条件,使得得到的结式严格为正,此时,可以获取满足条件的参数系数的取值,从而找到一个满足条件的秩函数,通过实验验证该秩函数探测方法的有效性。实验结果表明,利用该方法,可以有效地为多项式循环程序找到多项式秩函数,包括深度为d的多阶段多项式秩函数,与已有方法相比,该方法能够更高效地找到多项式秩函数,对于基于柱形代数分解( CAD)方法的探测方法因时间复杂度问题无法而应对的一些循环,利用所提方法能够在几秒内为这些循环找到秩函数。
发表期刊	计算机应用
ISSN	1001-9081
卷号	39期号:7页码:2065
收录类别	CSCD
CSCD记录号	CSCD:6530490
语种	英语