Abstract
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(nlog 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.
Original language | English |
---|---|
Article number | 14 |
Number of pages | 36 |
Journal | ACM Transactions on Programming Languages and Systems (TOPLAS) |
Volume | 44 |
Issue number | 3 |
Early online date | 15 Jul 2022 |
DOIs | |
Publication status | Published - 30 Sept 2022 |
Keywords
- 2023 OA procedure