Termination analysis of C programs is a challenging task. On the one hand, the analysis needs to be precise enough to draw meaningful conclusions. On the other hand, relevant programs in practice are large and require substantial abstraction. It is this inherent trade-off that is the crux of the problem. In this work, we present AProVE, a tool that uses symbolic execution to analyze termination of memory-manipulating C programs. While traditionally, AProVE's focus was on the preciseness of the analysis, we describe how we adapted our approach towards a modular analysis. Due to this adaption, our approach can now also handle recursive programs. Moreover, we present further performance improvements which we developed to make AProVE scale to large programs.

翻译：C程序的终止分析是一项具有挑战性的任务。一方面，分析需要足够精确以得出有意义的结论。另一方面，实际中的相关程序规模庞大，需要大量抽象。正是这种固有的权衡构成了问题的关键。在本文中，我们介绍工具AProVE，它利用符号执行来分析内存操作C程序的终止性。虽然传统上AProVE侧重于分析的精确性，但我们描述了如何将方法调整为模块化分析。得益于这一调整，我们的方法现在也能处理递归程序。此外，我们还展示了为进一步提升性能使AProVE可扩展至大型程序而开发的改进措施。