选择性分摊资源边界（扩展版）
Selectively-Amortized Resource Bounding (Extended Version)
摘要：
我们考虑自动证明资源界限的问题。也就是说，我们研究如何证明一个整数值的资源变量是有界的一个给定的程序表达式。由于许多重要的应用（例如，检测性能缺陷、防止算法复杂性攻击、识别侧信道漏洞），其中重点通常是开发精确的摊销推理技术以推断最准确的资源使用情况。虽然这种创新仍然至关重要，但我们观察到，完全精确的摊销并不总是证明利益界限所必需的。事实上，通过选择性地摊销，所需的支持不变量可以更简单，使不变量推理任务更可行和可预测。我们提出了一个框架，选择性摊还分析，混合最坏情况和摊销推理通过属性分解和程序转换。我们证明在任何这样的分解产生一个声音的资源约束在原程序中的界限，我们给出了一个算法，选择一个合理的分解。
英文摘要：
We consider the problem of automatically proving resource bounds. That is, we study how to prove that an integer-valued resource variable is bounded by a given program expression. Automatic resource-bound analysis has recently received significant attention because of a number of important applications (e.g., detecting performance bugs, preventing algorithmic-complexity attacks, identifying side-channel vulnerabilities), where the focus has often been on developing precise amortized reasoning techniques to infer the most exact resource usage. While such innovations remain critical, we observe that fully precise amortization is not always necessary to prove a bound of interest. And in fact, by amortizing selectively, the needed supporting invariants can be simpler, making the invariant inference task more feasible and predictable. We present a framework for selectively-amortized analysis that mixes worst-case and amortized reasoning via a property decomposition and a program transformation. We show that proving bounds in any such decomposition yields a sound resource bound in the original program, and we give an algorithm for selecting a reasonable decomposition.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
