Selectively-Amortized Resource Bounding
Selectively-Amortized Resource Bounding
复制标题
选择性摊销资源限制
DOI：
10.1007/978-3-030-88806-0_14
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Trivedi, Ashutosh
中科院分区：
文献类型：
--
作者：
Lu, Tianhan;Chang, Bor-Yuh Evan;Trivedi, Ashutosh
我们考虑自动证明资源界限的问题。也就是说，我们研究如何证明一个整数值的资源变量是有界的一个给定的程序表达式。由于许多重要的应用（例如，检测性能缺陷、防止算法复杂性攻击、识别侧信道漏洞），其中重点通常是开发精确的摊销推理技术以推断最准确的资源使用情况。虽然这种创新仍然至关重要，但我们观察到，完全精确的摊销并不总是证明利益界限所必需的。事实上，通过选择性地摊销，所需的支持不变量可以更简单，使不变量推理任务更可行和可预测。我们提出了一个框架，选择性摊销分析，混合最坏情况下，摊销推理通过属性分解和程序转换。我们证明在任何这样的分解产生一个声音的资源约束在原程序中的界限，我们给出了一个算法，选择一个合理的分解。
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 amortizingselectively, 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.
登录
查看更多内容
java字节码的堆空间分析
DOI：
10.1145/1296907.1296922
发表时间：
2007
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
E. Albert;S. Genaim;M. Gómez
通讯作者：
M. Gómez
DOI：
10.1137/0606031
发表时间：
1985-04
期刊：
Siam Journal on Algebraic and Discrete Methods
影响因子：
--
作者：
R. Tarjan
通讯作者：
R. Tarjan
DOI：
10.1007/978-3-030-11245-5_13
发表时间：
2018-10
期刊：
--
影响因子：
--
作者：
Tianhan Lu;Pavol Cerný;B. E. Chang;Ashutosh Trivedi
通讯作者：
Tianhan Lu;Pavol Cerný;B. E. Chang;Ashutosh Trivedi
更精确且适用范围更广的成本分析
DOI：
--
发表时间：
2011
期刊：
International Conference on Verification, Model Checking and Abstract Interpretation
影响因子：
--
作者：
E. Albert;S. Genaim;A. Masud
通讯作者：
A. Masud
数值循环的闭合形式
影响因子：
--
作者：
Zachary Kincaid;J. Breck;John Cyphert;T. Reps
通讯作者：
T. Reps