发明授权
- 专利标题: 基于界函数合成的循环程序终止性判断方法
-
申请号: CN202110173226.1申请日: 2021-02-04
-
公开(公告)号: CN112698891B公开(公告)日: 2023-10-31
- 发明人: 李轶 , 谭旺 , 杨文强
- 申请人: 中国科学院重庆绿色智能技术研究院
- 申请人地址: 重庆市北碚区水土镇水土高新园方正大道266号
- 专利权人: 中国科学院重庆绿色智能技术研究院
- 当前专利权人: 中国科学院重庆绿色智能技术研究院
- 当前专利权人地址: 重庆市北碚区水土镇水土高新园方正大道266号
- 主分类号: G06F9/448
- IPC分类号: G06F9/448
摘要:
本发明涉及基于界函数的循环程序终止性判断方法,属于计算机程序验证领域,包含以下步骤:S1、遍历程序,查找程序中的循环程序,对该循环程序的循环区域进行均匀采样;S2、设定界函数模板,将界函数问题转化为线性二分类问题,求得映射关系;S3、依次将样本点映射关系进行分类,并打上标签,得到训练集;S4、将训练集通过分类器进行训练,得到分类超平面,进而得到候选的界函数;S5、将候选界函数结合不变式量词消去进行验证,验证循环程序终止性。本发明针对不能通过现有秩函数方法来证明其终止性的循环程序能够给出终止性判定结果,其结果更加具有完备性。
公开/授权文献
- CN112698891A 基于界函数合成的循环程序终止性判断方法 公开/授权日:2021-04-23