计算机应用研究2026，Vol.43Issue(3)：641-650,10.DOI:10.19734/j.issn.1001-3695.2025.08.0277
基于秩函数合成的程序终止性验证综述
Survey on program termination based on ranking function synthesis
摘要
Abstract
Ranking function synthesis is one of the most widely used techniques for program termination verification.It proves program termination by constructing a well-founded mapping over program state transitions.In recent years,the application of deep learning techniques to the synthesis of ranking functions has shown phase progress,which has partially reduced the re-liance of formal approaches on expertise in program analysis and logical reasoning,while opening new perspectives for further exploration in this field.To provide a theoretical background and technical references for future studies,this paper introduced the fundamental concepts of ranking functions and then systematically reviewed representative work on single ranking func-tions,lexicographic ranking functions,multiphase ranking functions,and neural ranking functions,from both formal-method-based and learning-based perspectives.Based on this review,this paper collected program examples from existing studies and constructed a large-scale synthetic dataset of linear simple loops to support learning-based research.Finally,this paper dis-cussed potential directions for future research based on current limitations in dataset construction,network architecture,trai-ning strategies,and verification cost.关键词
程序终止性/秩函数合成/形式化方法/机器学习/深度学习/神经秩函数Key words
program termination/ranking function synthesis/formal methods/machine learning/deep learning/neural ranking function分类
信息技术与安全科学引用本文复制引用
蔡裕星,陈长波,李轶..基于秩函数合成的程序终止性验证综述[J].计算机应用研究,2026,43(3):641-650,10.基金项目
国家重点研发计划资助项目(2023YFA1009402) （2023YFA1009402）
重庆英才计划青年拔尖项目(2021000263) （2021000263）
