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}
}