基于秩函数合成的程序终止性验证综述OA

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.