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传统上的重点是分析的准确性, 但是我们描述我们如何调整我们的方法, 以进行模块分析。 由于这种调整, 我们的方法现在也可以处理循环程序。 此外, 我们提出进一步的绩效改进, 我们开发了AProeve, 以使大型方案成为AProve的规模 。
相关内容
微信扫码咨询专知VIP会员