Proving Termination Of Imperative Programs Using Max-Smt
2013 FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD)(2013)
摘要
We show how Max-SMT can be exploited in constraint-based program termination proving. Thanks to expressing the generation of a ranking function as a Max-SMT optimization problem where constraints are assigned different weights, quasi-ranking functions -functions that almost satisfy all conditions for ensuring well-foundedness- are produced in a lack of ranking functions. By means of trace partitioning, this allows our method to progress in the termination analysis where other approaches would get stuck. Moreover, Max-SMT makes it easy to combine the process of building the termination argument with the usually necessary task of generating supporting invariants. The method has been implemented in a prototype that has successfully been tested on a wide set of programs.
更多查看译文
关键词
computability,theorem proving,termination analysis
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络