基于插值的转移不变量生成的终止分析
Termination analysis with interpolation-based transition invariant generation
浏览论文内容
中文总结 AI 辅助
本文提出基于插值的转移不变量生成的终止分析方法，在GOLEM框架中实现并在TermComp基准测试上验证，可在统一框架内处理终止与非终止分析，性能与先进工具相当。
中文摘要 AI 辅助
无限状态系统的终止与非终止是互补问题，尽管联系紧密，但通常由不同技术处理。本文核心思路是连接终止与非终止分析，使二者共享中间结果并相互指导。我们提出一种基于良基转移不变量生成的新终止分析方法，利用Craig插值生成转移不变量，捕捉终止的结构原因。该技术扩展了基于安全性的非终止分析，使其能在统一框架内证明终止与非终止。我们在GOLEM验证框架中实现了该方法，并在Termination Competition（TermComp）的基准测试上进行评估。实验结果表明，结合终止与非终止分析是有益的，其性能可与最先进工具相媲美。
英文摘要
Termination and nontermination of infinite-state systems are complementary problems that, despite their close connection, are typically addressed by separate techniques. The core idea of this paper is to connect termination and nontermination analysis, enabling the two to share intermediate results and guide one another. We present a new termination analysis approach based on the generation of well-founded transition invariants. It leverages Craig interpolation for transition invariant generation, capturing the structural reasons for termination. The proposed technique extends safety-based nontermination analysis, enabling it to prove both termination and nontermination within a unified framework. We implemented our approach in the GOLEM verification framework and evaluated it on benchmarks from the Termination Competition (TermComp). Empirical results demonstrate that combining termination and nontermination is beneficial and yields performance comparable to state-of-the-art tools.
