基于符号执行和线性规划推导经验性资源边界（扩展版）
Inferring Empirical Sound Resource Bounds via Symbolic Execution and Linear Programming (Extended Version)
浏览论文内容
中文总结 AI 辅助
本文提出一种结合动态符号执行与混合整数线性规划的混合方法，实现了函数式程序最坏情况资源消耗经验性上界的推导，相关原型工具CompAS已在Zenodo公开。
中文摘要 AI 辅助
现有程序资源分析方法主要分为静态分析和动态分析两大范式：前者可提供形式化保证但本质上不完备；后者适用性广，但可能遗漏罕见但典型的最坏情况场景，因此缺乏可靠性。混合方法试图结合两种范式的优势，从而能够分析那些对于纯静态技术而言过于复杂，或动态方法面临组合爆炸问题的程序。本文提出一种新颖的混合方法，用于系统推导函数式程序最坏情况资源消耗的上界。该方法结合动态符号执行，在约束输入空间内穷尽探索所有可能的计算路径，并结合混合整数线性规划推导经验性可靠的上界。我们已将该方法实现为原型工具CompAS，并在Zenodo上公开了该工具。
英文摘要
Existing approaches to resource analysis of programs can be classified into two main paradigms: static analysis and dynamic analysis methods. The former allow for formal guarantees but are inherently incomplete; the latter are widely applicable but may miss rare but characteristic (worst-case) scenarios and thus lack soundness. Hybrid approaches attempt to combine the strengths of both paradigms, thereby enabling the analysis of programs that are either too complex for purely static techniques or where dynamic approaches suffer from combinatorial explosion. In this paper, we present a novel hybrid approach that systematically derives upper bounds for the worst-case resource consumption of functional programs. Our method combines dynamic symbolic execution to exhaustively explore all possible computation paths within a constrained input space with mixed-integer linear programming to derive empirically sound upper bounds. We have implemented the methodology in a prototype tool, dubbed CompAS, which we made available on Zenodo.
