When programs feature a complex control flow, existing techniques for
resource analysis produce cost relation systems (CRS) whose cost functions
retain the complex flow of the program and, consequently, might not be solvable
into closed-form upper bounds. This paper presents a novel approach to resource
analysis that is driven by the result of a termination analysis. The
fundamental idea is that the termination proof encapsulates the flows of the
program which are relevant for the cost computation so that, by driving the
generation of the CRS using the termination proof, we produce a
linearly-bounded CRS (LB-CRS). A LB-CRS is composed of cost functions that are
guaranteed to be locally bounded by linear ranking functions and thus greatly
simplify the process of CRS solving. We have built a new resource analysis
tool, named MaxCore, that is guided by the VeryMax termination analyzer and
uses CoFloCo and PUBS as CRS solvers. Our experimental results on the set of
benchmarks from the Complexity and Termination Competition 2019 for C Integer
programs show that MaxCore outperforms all other resource analysis tools. Under
consideration for acceptance in TPLP.

该论文提出了一种资源分析方法，它使用终止分析结果驱动成本关系系统（CRS）的生成，并且最终生成的线性有界 CRS（LB-CRS）克服了现有技术产生复杂程序流程的成本函数难以解决的问题，作者还制定了一种名为 MaxCore 的资源分析工具，并针对 C 整数程序的一组基准测试进行了实验，结果显示 MaxCore 优于其他所有资源分析工具。