We improve and refine a method for certifying that the values' sizes computed by an imperative program will be bounded by polynomials in the program's inputs' sizes. Our work ''tames'' the non-determinism of the original analysis, and offers an innovative way of completing the analysis when a non-polynomial growth is found. We furthermore enrich the analyzed language by adding function definitions and calls, allowing to compose the analysis of different libraries and offering generally more modularity. The implementation of our improved method, discussed in a tool paper [2], also required to reason about the efficiency of some of the needed operations on the matrices produced by the analysis. It is our hope that this work will enable and facilitate static analysis of source code to guarantee its correctness with respect to resource usages.

翻译：我们改进和完善了一种方法,以证明由紧急方案计算的价值大小将受方案投入大小中多面体的束缚。我们的工作“数据”没有确定原始分析的不确定性,并且提供了一种创新的方法,在发现非垄断增长时完成分析。我们还通过添加功能定义和电话来丰富所分析的语言,从而能够对不同的图书馆进行分析,并普遍提供更多的模块性。实施工具文件[2]中讨论的改进方法,还需要说明分析所制作的矩阵上某些所需操作的效率。我们希望这项工作将促成并促进源代码的静态分析,以保证源代码在资源使用方面的正确性。