基于界函数合成的循环程序终止性判断方法
摘要:
本发明涉及基于界函数的循环程序终止性判断方法,属于计算机程序验证领域,包含以下步骤:S1、遍历程序,查找程序中的循环程序,对该循环程序的循环区域进行均匀采样;S2、设定界函数模板,将界函数问题转化为线性二分类问题,求得映射关系;S3、依次将样本点映射关系进行分类,并打上标签,得到训练集;S4、将训练集通过分类器进行训练,得到分类超平面,进而得到候选的界函数;S5、将候选界函数结合不变式量词消去进行验证,验证循环程序终止性。本发明针对不能通过现有秩函数方法来证明其终止性的循环程序能够给出终止性判定结果,其结果更加具有完备性。
公开/授权文献
0/0