基于秩函数合成的程序终止性验证综述
Survey on program termination based on ranking function synthesis
1. 中国科学院重庆绿色智能技术研究院, 重庆 400714
2. 中国科学院大学 重庆学院, 重庆 400714
3. 重庆邮电大学 计算机科学与技术学院, 重庆 400065
摘要
秩函数合成是程序终止性验证的主流方法之一，其基本思想是通过构造程序变量状态变换的良序映射来证明程序的终止性。近年来，深度学习技术在秩函数合成中的应用取得了初步进展，在一定程度上缓解了形式化方法对程序分析与逻辑推理等专业知识的依赖，同时为该领域的进一步研究提供了新的思路。为给后续研究提供理论背景和技术参考，首先介绍了秩函数的基本概念，从基于形式化方法和基于学习方法两个方面出发，系统梳理了单一秩函数、字典序秩函数、多阶段秩函数以及神经秩函数合成的代表性工作。在此基础上，收集了相关研究中的程序样例，构建并公开了一个大规模的线性简单循环人工合成数据集，为基于学习方法的研究提供数据支持。最后，针对现有研究在数据集构造、网络结构与训练策略、验证成本等方面的不足，对未来的研究方向进行了展望。
基金项目
国家重点研发计划(2023YFA1009402)
重庆英才计划青年拔尖项目(2021000263)
出版信息
DOI: 10.19734/j.issn.1001-3695.2025.08.0277
出版期卷: 《计算机应用研究》 优先出版, 2026年第43卷 第3期
发布历史
[2025-11-18] 优先出版
引用本文
蔡裕星, 陈长波, 李轶. 基于秩函数合成的程序终止性验证综述 [J]. 计算机应用研究, 2026, 43 (3). (2025-11-18). https://doi.org/10.19734/j.issn.1001-3695.2025.08.0277. (Cai Yuxing, Chen Changbo, Li Yi. Survey on program termination based on ranking function synthesis [J]. Application Research of Computers, 2026, 43 (3). (2025-11-18). https://doi.org/10.19734/j.issn.1001-3695.2025.08.0277. )
关于期刊
- 计算机应用研究 月刊
- Application Research of Computers
-
刊号
ISSN 1001-3695
CN 51-1196/TP
《计算机应用研究》创刊于1984年，是由四川省科技厅所属四川省计算机研究院主办的计算技术类学术刊物。
《计算机应用研究》瞄准本学科领域迫切需要的前沿技术，及时反映国内外计算机应用研究的主流技术、热点技术及最新发展趋势。主要刊载内容包括本学科领域高水平的学术论文、本学科最新科研成果和重大应用成果。栏目内容涉及计算机学科新理论、计算机基础理论、算法理论研究、算法设计与分析、区块链技术、系统软件与软件工程技术、模式识别与人工智能、体系结构、先进计算、并行处理、数据库技术、计算机网络与通信技术、信息安全技术、计算机图像图形学及其最新热点应用技术。
《计算机应用研究》拥有众多高层次读者、作者，读者对象主要为从事计算机学科领域高、中级研究人员及工程技术人员，各高等院校计算机专业及相关专业的师生。多年来《计算机应用研究》的总被引频次及Web下载率一直名列本学科同类学术刊物前茅，所刊发的学术论文以其新颖性、学术性、前瞻性、导向性、实用性而备受广大读者的喜爱。
收录和评价
- 第二届国家期刊奖百种重点期刊
- 中国期刊方阵双效期刊
- 全国中文核心期刊（北大2023年版）
- 中国科技核心期刊
- 中国科学引文数据库(CSCD)来源期刊
- RCCSE中国核心学术期刊
- 中国计算机学会会刊
- 2020—2022年科技期刊世界影响力指数(WJCI)报告收录期刊
- 中国科技期刊精品数据库全文来源期刊
- 中国学术期刊综合评价数据库来源期刊
- 《中国期刊网》《中国学术期刊(光盘版)》来源期刊
- 2017—2019年中国国际影响力优秀学术期刊(自然科学与工程技术)
- 中国精品科技期刊顶尖学术论文(F5000)项目来源期刊
- 《中国工程技术电子信息网》《电子科技文献数据库》来源期刊
- 英国《科学文摘》(INSPEC)来源期刊
- 《日本科学技术振兴机构数据库》(JST)来源期刊
- 俄罗斯《文摘杂志》(AJ, VINITI)来源期刊
- 美国《艾博思科学术数据库》(EBSCO)全文来源期刊
- 美国《剑桥科学文摘(自然科学)》(CSA(NS))核心期刊
- 波兰《哥白尼索引》(IC)来源期刊
- 美国《乌利希期刊指南(网络版)》(Ulrichsweb)收录期刊
