一句话：提出基于资源货币的逐步精化框架，在 LLVM IR 上验证高效算法的功能正确性与（摊还）最坏情况复杂度。
本文提出一个验证框架，用于同时验证实际高效算法的功能正确性和（摊还）最坏情况复杂度。其核心是逐步精化方法与新提出的“资源货币”概念：资源货币让复杂度分析沿精化链自然组织，并支持对操作计数的细粒度分析。框架以 LLVM 中间表示为目标，在已有语义基础上加入代价模型。作者通过两个案例研究进行评估：动态数组 push 的摊还常数时间操作，以及 O(n log n) 的 introsort 算法，并将它们精化到高效 LLVM 实现。所得排序算法性能与 GNU C++ 标准库中的先进实现相当，且可证明满足 C++ 标准要求的复杂度。
We present a framework to verify both, functional correctness and (amortized) worst-case complexity of practically efficient algorithms. We implemented a stepwise refinement approach, using the novel concept of resource currencies to naturally structure the resource analysis along the refinement chain, and allow a fine-grained analysis of operation counts. Our framework targets the LLVM intermediate representation. We extend its semantics from earlier work with a cost model. As case studies, we verify the amortized constant time push operation on dynamic arrays and the O ( n log n ) introsort algorithm, and refine them down to efficient LLVM implementations. Our sorting algorithm performs on par with the state-of-the-art implementation found in the GNU C++ Library, and provably satisfies the complexity required by the C++ standard.
@article{paperbot1609,
title = {For a Few Dollars More: Verified Fine-Grained Algorithm Analysis Down to LLVM},
author = {Maximilian P. L. Haslbeck and Peter Lammich},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {44},
number = {3},
year = {2022},
doi = {10.1145/3486169}
}